diff options
50 files changed, 3524 insertions, 1231 deletions
@@ -282,6 +282,14 @@ SOURCE=.\src\base\seq\seq.h # End Source File # Begin Source File +SOURCE=.\src\base\seq\seqAigCore.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\seq\seqAigIter.c +# End Source File +# Begin Source File + SOURCE=.\src\base\seq\seqCreate.c # End Source File # Begin Source File @@ -1698,10 +1706,6 @@ SOURCE=.\src\misc\vec\vec.h # End Source File # Begin Source File -SOURCE=.\src\misc\vec\vecFan.h -# End Source File -# Begin Source File - SOURCE=.\src\misc\vec\vecInt.h # End Source File # Begin Source File Binary files differ@@ -6,13 +6,13 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1416.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1A31.tmp" with contents [ /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c -"C:\_projects\abc\src\base\seq\seqFpgaIter.c" +"C:\_projects\abc\src\base\seq\seqRetCore.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1416.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1417.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1A31.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1A32.tmp" with contents [ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept .\Debug\abcAig.obj @@ -64,8 +64,6 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\seqMan.obj .\Debug\seqMapCore.obj .\Debug\seqMapIter.obj -.\Debug\seqRetCore.obj -.\Debug\seqRetIter.obj .\Debug\seqShare.obj .\Debug\seqUtil.obj .\Debug\cmd.obj @@ -328,13 +326,17 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\mvcPrint.obj .\Debug\mvcSort.obj .\Debug\mvcUtils.obj +.\Debug\seqRetCore.obj +.\Debug\seqRetIter.obj +.\Debug\seqAigCore.obj +.\Debug\seqAigIter.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1417.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1A32.tmp" <h3>Output Window</h3> Compiling... -seqFpgaIter.c +seqRetCore.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1418.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1A33.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abcAig.sbr @@ -386,8 +388,6 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1418.tmp" with cont .\Debug\seqMan.sbr .\Debug\seqMapCore.sbr .\Debug\seqMapIter.sbr -.\Debug\seqRetCore.sbr -.\Debug\seqRetIter.sbr .\Debug\seqShare.sbr .\Debug\seqUtil.sbr .\Debug\cmd.sbr @@ -649,8 +649,12 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1418.tmp" with cont .\Debug\mvcOpBool.sbr .\Debug\mvcPrint.sbr .\Debug\mvcSort.sbr -.\Debug\mvcUtils.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1418.tmp" +.\Debug\mvcUtils.sbr +.\Debug\seqRetCore.sbr +.\Debug\seqRetIter.sbr +.\Debug\seqAigCore.sbr +.\Debug\seqAigIter.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1A33.tmp" Creating browse info file... <h3>Output Window</h3> @@ -22,6 +22,8 @@ alias clp collapse alias esd ext_seq_dcs alias f fraig alias fs fraig_sweep +alias fsto fraig_store +alias fres fraig_restore alias ft fraig_trust alias mu renode -m alias pex print_exdc -d diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 1985f4c8..1904a0b6 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -104,12 +104,12 @@ typedef enum { #define bool int #endif -typedef struct Abc_Obj_t_ Abc_Obj_t; -typedef struct Abc_Ntk_t_ Abc_Ntk_t; -typedef struct Abc_Aig_t_ Abc_Aig_t; -typedef struct Abc_ManTime_t_ Abc_ManTime_t; -typedef struct Abc_ManCut_t_ Abc_ManCut_t; -typedef struct Abc_Time_t_ Abc_Time_t; +typedef struct Abc_Obj_t_ Abc_Obj_t; +typedef struct Abc_Ntk_t_ Abc_Ntk_t; +typedef struct Abc_Aig_t_ Abc_Aig_t; +typedef struct Abc_ManTime_t_ Abc_ManTime_t; +typedef struct Abc_ManCut_t_ Abc_ManCut_t; +typedef struct Abc_Time_t_ Abc_Time_t; struct Abc_Time_t_ { @@ -122,19 +122,21 @@ struct Abc_Obj_t_ // 12 words { // high-level information Abc_Ntk_t * pNtk; // the host network - unsigned Type : 4; // the object type - unsigned fExor : 1; // marks AIG node that is a root of EXOR - unsigned Id : 27; // the ID of the object + int Id; // the object ID // internal information + unsigned Type : 3; // the object type unsigned fMarkA : 1; // the multipurpose mark unsigned fMarkB : 1; // the multipurpose mark unsigned fMarkC : 1; // the multipurpose mark unsigned fPhase : 1; // the flag to mark the phase of equivalent node - unsigned TravId : 12; // the traversal ID - unsigned Level : 16; // the level of the node + unsigned fExor : 1; // marks AIG node that is a root of EXOR + unsigned fCompl0 : 1; // complemented attribute of the first fanin in the AIG + unsigned fCompl1 : 1; // complemented attribute of the second fanin in the AIG + unsigned TravId : 10; // the traversal ID (if changed, update Abc_NtkIncrementTravId) + unsigned Level : 12; // the level of the node // connectivity - Vec_Fan_t vFanins; // the array of fanins - Vec_Fan_t vFanouts; // the array of fanouts + Vec_Int_t vFanins; // the array of fanins + Vec_Int_t vFanouts; // the array of fanouts // miscellaneous void * pData; // the network specific data (SOP, BDD, gate, equiv class, etc) Abc_Obj_t * pNext; // the next pointer in the hash table @@ -268,8 +270,8 @@ static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i ) { assert( i static inline unsigned Abc_ObjType( Abc_Obj_t * pObj ) { return pObj->Type; } static inline unsigned Abc_ObjId( Abc_Obj_t * pObj ) { return pObj->Id; } static inline int Abc_ObjTravId( Abc_Obj_t * pObj ) { return pObj->TravId; } -static inline Vec_Fan_t * Abc_ObjFaninVec( Abc_Obj_t * pObj ) { return &pObj->vFanins; } -static inline Vec_Fan_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj ) { return &pObj->vFanouts; } +static inline Vec_Int_t * Abc_ObjFaninVec( Abc_Obj_t * pObj ) { return &pObj->vFanins; } +static inline Vec_Int_t * Abc_ObjFanoutVec( Abc_Obj_t * pObj ) { return &pObj->vFanouts; } static inline Abc_Obj_t * Abc_ObjCopy( Abc_Obj_t * pObj ) { return pObj->pCopy; } static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj ) { return pObj->pNtk; } static inline void * Abc_ObjData( Abc_Obj_t * pObj ) { return pObj->pData; } @@ -298,28 +300,28 @@ static inline bool Abc_ObjIsCio( Abc_Obj_t * pObj ) { return pO // working with fanin/fanout edges static inline int Abc_ObjFaninNum( Abc_Obj_t * pObj ) { return pObj->vFanins.nSize; } static inline int Abc_ObjFanoutNum( Abc_Obj_t * pObj ) { return pObj->vFanouts.nSize; } -static inline int Abc_ObjFaninId( Abc_Obj_t * pObj, int i) { return pObj->vFanins.pArray[i].iFan; } -static inline int Abc_ObjFaninId0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].iFan; } -static inline int Abc_ObjFaninId1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].iFan; } -static inline int Abc_ObjFanoutEdgeNum( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) { assert( Abc_NtkHasAig(pObj->pNtk) ); if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) return 0; if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) return 1; assert( 0 ); return -1; } -static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; } -static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj); } -static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj); } -static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ) { return pObj->vFanins.pArray[i].fCompl; } -static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].fCompl; } -static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].fCompl; } +static inline int Abc_ObjFaninId( Abc_Obj_t * pObj, int i) { return pObj->vFanins.pArray[i]; } +static inline int Abc_ObjFaninId0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0]; } +static inline int Abc_ObjFaninId1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1]; } +static inline int Abc_ObjFanoutEdgeNum( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) { assert( Abc_NtkHasAig(pObj->pNtk) ); if ( Abc_ObjFaninId0(pFanout) == pObj->Id ) return 0; if ( Abc_ObjFaninId1(pFanout) == pObj->Id ) return 1; assert( 0 ); return -1; } +static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i] ]; } +static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0] ]; } +static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i] ]; } +static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0] ]; } +static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1] ]; } +static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj); } +static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj ) { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj); } +static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->fCompl0; } +static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->fCompl1; } +static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ) { assert( i >=0 && i < 2 ); return i? pObj->fCompl1 : pObj->fCompl0; } +static inline void Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ assert( i >=0 && i < 2 ); if ( i ) pObj->fCompl1 = 1; else pObj->fCompl0 = 1; } +static inline void Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ assert( i >=0 && i < 2 ); if ( i ) pObj->fCompl1^= 1; else pObj->fCompl0^= 1; } static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );} static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) ); } static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) ); } -static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) );} -static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); } -static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ); } -static inline void Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1; } -static inline void Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1; } +static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) ); } +static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); } +static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ); } // checking the node type static inline bool Abc_NodeIsAigAnd( Abc_Obj_t * pNode ) { assert(Abc_NtkHasAig(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2; } @@ -473,6 +475,7 @@ extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk ); /*=== abcLatch.c ==========================================================*/ extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch ); extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk ); +extern int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk ); /*=== abcMap.c ==========================================================*/ extern int Abc_NtkUnmap( Abc_Ntk_t * pNtk ); /*=== abcMiter.c ==========================================================*/ diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 9f5ebb64..53ad88c2 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -394,13 +394,15 @@ Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) ***********************************************************************/ void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis ) { - Abc_Obj_t * pAnd, ** ppPlace; + Abc_Obj_t * pAnd, * pAnd0, * pAnd1, ** ppPlace; unsigned Key; assert( !Abc_ObjIsComplement(pThis) ); assert( Abc_ObjIsNode(pThis) ); assert( Abc_ObjFaninNum(pThis) == 2 ); assert( pMan->pNtkAig == pThis->pNtk ); // get the hash key for these two nodes + pAnd0 = Abc_ObjRegular( Abc_ObjChild0(pThis) ); + pAnd1 = Abc_ObjRegular( Abc_ObjChild1(pThis) ); Key = Abc_HashKey2( Abc_ObjChild0(pThis), Abc_ObjChild1(pThis), pMan->nBins ); // find the matching node in the table ppPlace = pMan->pBins + Key; @@ -479,7 +481,7 @@ void Abc_AigRehash( Abc_Aig_t * pMan ) { Abc_Obj_t ** pBinsNew; Abc_Obj_t * pEnt, * pEnt2; - Abc_Fan_t * pArray; + int * pArray; unsigned Key; int Counter, Temp, i; @@ -493,14 +495,14 @@ void Abc_AigRehash( Abc_Aig_t * pMan ) { // swap the fanins if needed pArray = pEnt->vFanins.pArray; - if ( pArray[0].iFan > pArray[1].iFan ) + if ( pArray[0] > pArray[1] ) { - Temp = pArray[0].iFan; - pArray[0].iFan = pArray[1].iFan; - pArray[1].iFan = Temp; - Temp = pArray[0].fCompl; - pArray[0].fCompl = pArray[1].fCompl; - pArray[1].fCompl = Temp; + Temp = pArray[0]; + pArray[0] = pArray[1]; + pArray[1] = Temp; + Temp = pEnt->fCompl0; + pEnt->fCompl0 = pEnt->fCompl1; + pEnt->fCompl1 = Temp; } // rehash the node Key = Abc_HashKey2( Abc_ObjChild0(pEnt), Abc_ObjChild1(pEnt), pMan->nBins ); @@ -660,7 +662,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel ) continue; } // find the old node as a fanin of this fanout - iFanin = Vec_FanFindEntry( &pFanout->vFanins, pOld->Id ); + iFanin = Vec_IntFind( &pFanout->vFanins, pOld->Id ); assert( iFanin == 0 || iFanin == 1 ); // get the new fanin pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) ); @@ -1009,7 +1011,7 @@ bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode ) int i, iFanin; Abc_ObjForEachFanout( pNode, pFanout, i ) { - iFanin = Vec_FanFindEntry( &pFanout->vFanins, pNode->Id ); + iFanin = Vec_IntFind( &pFanout->vFanins, pNode->Id ); assert( iFanin >= 0 ); if ( Abc_ObjFaninC( pFanout, iFanin ) ) return 1; @@ -1038,7 +1040,7 @@ bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ) { if ( !Abc_NodeIsTravIdCurrent(pFanout) ) continue; - iFanin = Vec_FanFindEntry( &pFanout->vFanins, pNode->Id ); + iFanin = Vec_IntFind( &pFanout->vFanins, pNode->Id ); assert( iFanin >= 0 ); if ( Abc_ObjFaninC( pFanout, iFanin ) ) return 1; diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 548a2294..0211e9f8 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -417,7 +417,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) // go through the fanins of the object and make sure fanins have this object as a fanout Abc_ObjForEachFanin( pObj, pFanin, i ) { - if ( Vec_FanFindEntry( &pFanin->vFanouts, pObj->Id ) == -1 ) + if ( Vec_IntFind( &pFanin->vFanouts, pObj->Id ) == -1 ) { fprintf( stdout, "NodeCheck: Object \"%s\" has fanin ", Abc_ObjName(pObj) ); fprintf( stdout, "\"%s\" but the fanin does not have it as a fanout.\n", Abc_ObjName(pFanin) ); @@ -427,7 +427,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) // go through the fanouts of the object and make sure fanouts have this object as a fanin Abc_ObjForEachFanout( pObj, pFanout, i ) { - if ( Vec_FanFindEntry( &pFanout->vFanins, pObj->Id ) == -1 ) + if ( Vec_IntFind( &pFanout->vFanins, pObj->Id ) == -1 ) { fprintf( stdout, "NodeCheck: Object \"%s\" has fanout ", Abc_ObjName(pObj) ); fprintf( stdout, "\"%s\" but the fanout does not have it as a fanin.\n", Abc_ObjName(pFanout) ); @@ -441,7 +441,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) // make sure fanins are not duplicated for ( i = 0; i < pObj->vFanins.nSize; i++ ) for ( k = i + 1; k < pObj->vFanins.nSize; k++ ) - if ( pObj->vFanins.pArray[k].iFan == pObj->vFanins.pArray[i].iFan ) + if ( pObj->vFanins.pArray[k] == pObj->vFanins.pArray[i] ) { printf( "Warning: Node %s has", Abc_ObjName(pObj) ); printf( " duplicated fanin %s.\n", Abc_ObjName(Abc_ObjFanin(pObj,k)) ); @@ -454,7 +454,7 @@ bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ) // make sure fanouts are not duplicated for ( i = 0; i < pObj->vFanouts.nSize; i++ ) for ( k = i + 1; k < pObj->vFanouts.nSize; k++ ) - if ( pObj->vFanouts.pArray[k].iFan == pObj->vFanouts.pArray[i].iFan ) + if ( pObj->vFanouts.pArray[k] == pObj->vFanouts.pArray[i] ) { printf( "Warning: Node %s has", Abc_ObjName(pObj) ); printf( " duplicated fanout %s.\n", Abc_ObjName(Abc_ObjFanout(pObj,k)) ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index dbd3e5fa..158edf65 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -221,6 +221,7 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode, * pFanin; int i, k; + assert( !Abc_NtkIsSeq(pNtk) ); // set the traversal ID Abc_NtkIncrementTravId( pNtk ); // mark the CIs @@ -229,11 +230,16 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk ) // go through the nodes Abc_NtkForEachNode( pNtk, pNode, i ) { + // check the fanins of the node Abc_ObjForEachFanin( pNode, pFanin, k ) - { if ( !Abc_NodeIsTravIdCurrent(pFanin) ) return 0; - } + // check the choices of the node + if ( Abc_NtkIsStrash(pNtk) && Abc_NodeIsAigChoice(pNode) ) + for ( pFanin = pNode->pData; pFanin; pFanin = pFanin->pData ) + if ( !Abc_NodeIsTravIdCurrent(pFanin) ) + return 0; + // mark the node as visited Abc_NodeSetTravIdCurrent( pNode ); } return 1; diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c index 983d41e4..59dff196 100644 --- a/src/base/abc/abcFanio.c +++ b/src/base/abc/abcFanio.c @@ -25,8 +25,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_LARGE_ID ((1<<24)-1) // should correspond to value in "vecFan.h" - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -48,10 +46,8 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) assert( !Abc_ObjIsComplement(pObj) ); assert( pObj->pNtk == pFaninR->pNtk ); assert( pObj->Id >= 0 && pFaninR->Id >= 0 ); - assert( pObj->Id < ABC_LARGE_ID ); // created but forgot to add it to the network? - assert( pFaninR->Id < ABC_LARGE_ID ); // created but forgot to add it to the network? - Vec_FanPush( pObj->pNtk->pMmStep, &pObj->vFanins, Vec_Int2Fan(pFaninR->Id) ); - Vec_FanPush( pObj->pNtk->pMmStep, &pFaninR->vFanouts, Vec_Int2Fan(pObj->Id) ); + Vec_IntPushMem( pObj->pNtk->pMmStep, &pObj->vFanins, pFaninR->Id ); + Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id ); if ( Abc_ObjIsComplement(pFanin) ) Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 ); } @@ -74,14 +70,12 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) assert( !Abc_ObjIsComplement(pFanin) ); assert( pObj->pNtk == pFanin->pNtk ); assert( pObj->Id >= 0 && pFanin->Id >= 0 ); - assert( pObj->Id < ABC_LARGE_ID ); // created but forgot to add it to the network? - assert( pFanin->Id < ABC_LARGE_ID ); // created but forgot to add it to the network? - if ( !Vec_FanDeleteEntry( &pObj->vFanins, pFanin->Id ) ) + if ( !Vec_IntRemove( &pObj->vFanins, pFanin->Id ) ) { printf( "The obj %d is not found among the fanins of obj %d ...\n", pFanin->Id, pObj->Id ); return; } - if ( !Vec_FanDeleteEntry( &pFanin->vFanouts, pObj->Id ) ) + if ( !Vec_IntRemove( &pFanin->vFanouts, pObj->Id ) ) { printf( "The obj %d is not found among the fanouts of obj %d ...\n", pObj->Id, pFanin->Id ); return; @@ -102,16 +96,19 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) ***********************************************************************/ void Abc_ObjRemoveFanins( Abc_Obj_t * pObj ) { - Vec_Fan_t * vFaninsOld; + Vec_Int_t * vFaninsOld; Abc_Obj_t * pFanin; int k; // remove old fanins vFaninsOld = &pObj->vFanins; for ( k = vFaninsOld->nSize - 1; k >= 0; k-- ) { - pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k].iFan ); + pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k] ); Abc_ObjDeleteFanin( pObj, pFanin ); } + pObj->fCompl0 = 0; + pObj->fCompl1 = 0; + assert( vFaninsOld->nSize == 0 ); } /**Function************************************************************* @@ -131,7 +128,7 @@ void Abc_ObjRemoveFanins( Abc_Obj_t * pObj ) void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew ) { Abc_Obj_t * pFaninNewR = Abc_ObjRegular(pFaninNew); - int iFanin, fCompl, nLats; + int iFanin, nLats;//, fCompl; assert( !Abc_ObjIsComplement(pObj) ); assert( !Abc_ObjIsComplement(pFaninOld) ); assert( pFaninOld != pFaninNewR ); @@ -139,29 +136,33 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa // assert( pObj != pFaninNewR ); assert( pObj->pNtk == pFaninOld->pNtk ); assert( pObj->pNtk == pFaninNewR->pNtk ); - if ( (iFanin = Vec_FanFindEntry( &pObj->vFanins, pFaninOld->Id )) == -1 ) + if ( (iFanin = Vec_IntFind( &pObj->vFanins, pFaninOld->Id )) == -1 ) { printf( "Node %s is not among", Abc_ObjName(pFaninOld) ); printf( " the fanins of node %s...\n", Abc_ObjName(pObj) ); return; } + // remember the attributes of the old fanin - fCompl = Abc_ObjFaninC(pObj, iFanin); +// fCompl = Abc_ObjFaninC(pObj, iFanin); // replace the old fanin entry by the new fanin entry (removes attributes) - Vec_FanWriteEntry( &pObj->vFanins, iFanin, Vec_Int2Fan(pFaninNewR->Id) ); + Vec_IntWriteEntry( &pObj->vFanins, iFanin, pFaninNewR->Id ); // set the attributes of the new fanin - if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) ) - Abc_ObjSetFaninC( pObj, iFanin ); +// if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) ) +// Abc_ObjSetFaninC( pObj, iFanin ); + if ( Abc_ObjIsComplement(pFaninNew) ) + Abc_ObjXorFaninC( pObj, iFanin ); + if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) ) Seq_ObjSetFaninL( pObj, iFanin, nLats ); // update the fanout of the fanin - if ( !Vec_FanDeleteEntry( &pFaninOld->vFanouts, pObj->Id ) ) + if ( !Vec_IntRemove( &pFaninOld->vFanouts, pObj->Id ) ) { printf( "Node %s is not among", Abc_ObjName(pObj) ); printf( " the fanouts of its old fanin %s...\n", Abc_ObjName(pFaninOld) ); // return; } - Vec_FanPush( pObj->pNtk->pMmStep, &pFaninNewR->vFanouts, Vec_Int2Fan(pObj->Id) ); + Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninNewR->vFanouts, pObj->Id ); } /**Function************************************************************* diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index a31f0b16..85dd9d8e 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -89,7 +89,38 @@ int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk ) int i, Counter; Counter = 0; Abc_NtkForEachLatch( pNtk, pLatch, i ) + { +// if ( Abc_NtkLatchIsSelfFeed(pLatch) && Abc_ObjFanoutNum(pLatch) > 1 ) +// printf( "Fanouts = %d.\n", Abc_ObjFanoutNum(pLatch) ); Counter += Abc_NtkLatchIsSelfFeed( pLatch ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Replaces self-feeding latches by latches with constant inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pLatch; + int i, Counter; + Counter = 0; + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + if ( Abc_NtkLatchIsSelfFeed( pLatch ) ) + { + Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(pLatch), Abc_NtkConst1(pNtk) ); + Counter++; + } + } return Counter; } diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 9d649f6f..39184e01 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -326,6 +326,10 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) Seq_NodeDupLats( pObj->pCopy, pObj, k ); } } + // relink the choice nodes + Abc_AigForEachAnd( pNtk, pObj, i ) + if ( pObj->pData ) + pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy; } else { diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index b144066f..481b069f 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -47,9 +47,9 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) Abc_Obj_t * pObj; pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj ); memset( pObj, 0, sizeof(Abc_Obj_t) ); - pObj->Id = -1; pObj->pNtk = pNtk; pObj->Type = Type; + pObj->Id = -1; return pObj; } diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 5d7b4302..8e1615d7 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -49,7 +49,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; int i; - if ( pNtk->nTravIds == (1<<12)-1 ) + if ( pNtk->nTravIds == (1<<10)-1 ) { pNtk->nTravIds = 0; Abc_NtkForEachObj( pNtk, pObj, i ) @@ -260,7 +260,7 @@ int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode; int i, Counter; - if ( !Abc_NtkIsStrash(pNtk) ) + if ( !Abc_NtkHasAig(pNtk) ) return 0; Counter = 0; Abc_NtkForEachNode( pNtk, pNode, i ) @@ -966,7 +966,7 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) Vec_PtrPush( vObjsNew, pNode ); } // finally, internal nodes in the DFS order - vNodes = Abc_NtkDfs( pNtk, 1 ); + vNodes = Abc_AigDfs( pNtk, 1, 0 ); Vec_PtrForEachEntry( vNodes, pNode, i ) { if ( pNode == pConst1 ) @@ -981,9 +981,9 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) Abc_NtkForEachObj( pNtk, pNode, i ) { Abc_ObjForEachFanin( pNode, pTemp, k ) - pNode->vFanins.pArray[k].iFan = pTemp->Id; + pNode->vFanins.pArray[k] = pTemp->Id; Abc_ObjForEachFanout( pNode, pTemp, k ) - pNode->vFanouts.pArray[k].iFan = pTemp->Id; + pNode->vFanouts.pArray[k] = pTemp->Id; } // replace the array of objs diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f7e7f763..0b24b3ff 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -4741,7 +4741,7 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c, nLoops; + int c;//, nLoops; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -4778,11 +4778,11 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) ) - { - fprintf( pErr, "Cannot create sequential AIG because the network contains %d self-feeding latches.\n", nLoops ); - return 0; - } +// if ( nLoops = Abc_NtkCountSelfFeedLatches(pNtk) ) +// { +// fprintf( pErr, "Cannot create sequential AIG because the network contains %d self-feeding latches.\n", nLoops ); +// return 0; +// } // get the new network pNtkRes = Abc_NtkAigToSeq( pNtk ); @@ -4854,8 +4854,8 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv ) } // share the latches on the fanout edges - if ( fShare ) - Seq_NtkShareFanouts(pNtk); +// if ( fShare ) +// Seq_NtkShareFanouts(pNtk); // get the new network pNtkRes = Abc_NtkSeqToLogicSop( pNtk ); @@ -4983,7 +4983,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c; + int c, nMaxIters; int fVerbose; pNtk = Abc_FrameReadNet(pAbc); @@ -4991,12 +4991,24 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 0; + nMaxIters = 15; + fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { + case 'I': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" ); + goto usage; + } + nMaxIters = atoi(argv[util_optind]); + util_optind++; + if ( nMaxIters < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -5020,7 +5032,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Seq_NtkFpgaMapRetime( pNtk, fVerbose ); + pNtkRes = Seq_NtkFpgaMapRetime( pNtk, nMaxIters, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); @@ -5031,10 +5043,11 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sfpga [-vh]\n" ); - fprintf( pErr, "\t performs integrated sequential FPGA mapping\n" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "usage: sfpga [-I num] [-vh]\n" ); + fprintf( pErr, "\t performs integrated sequential FPGA mapping\n" ); + fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -5053,21 +5066,32 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c; + int c, nMaxIters; int fVerbose; - extern Abc_Ntk_t * Abc_NtkMapSeq( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 1; + nMaxIters = 15; + fVerbose = 1; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { + case 'I': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" ); + goto usage; + } + nMaxIters = atoi(argv[util_optind]); + util_optind++; + if ( nMaxIters < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -5089,17 +5113,14 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Sequential standard cell mapping works only for sequential AIG (run \"seq\").\n" ); return 1; } - - printf( "This command is not yet implemented.\n" ); - return 0; - - +// printf( "This command is not yet implemented.\n" ); +// return 0; // get the new network - pNtkRes = Abc_NtkMapSeq( pNtk, fVerbose ); + pNtkRes = Seq_MapRetime( pNtk, nMaxIters, fVerbose ); if ( pNtkRes == NULL ) { - fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); + fprintf( pErr, "Sequential standard-cell mapping has failed.\n" ); return 1; } // replace the current network @@ -5107,10 +5128,11 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: smap [-vh]\n" ); - fprintf( pErr, "\t performs integrated sequential standard-cell mapping" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "usage: smap [-I num] [-vh]\n" ); + fprintf( pErr, "\t performs integrated sequential standard-cell mapping" ); + fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c index d97d50c5..78573718 100644 --- a/src/base/abci/abcAttach.c +++ b/src/base/abci/abcAttach.c @@ -187,7 +187,7 @@ int Abc_NodeAttach( Abc_Obj_t * pNode, Mio_Gate_t ** ppGates, unsigned ** puTrut Abc_ObjForEachFanin( pNode, pFanin, i ) pTempInts[i] = pFanin->Id; for ( i = 0; i < nFanins; i++ ) - pNode->vFanins.pArray[Perm[i]].iFan = pTempInts[i]; + pNode->vFanins.pArray[Perm[i]] = pTempInts[i]; // set the gate pNode->pCopy = (Abc_Obj_t *)pGate; return 1; diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index f285495c..3e34602d 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -185,12 +185,14 @@ void Abc_NtkCutsOracle( Abc_Ntk_t * pNtk, Cut_Oracle_t * p ) Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) { Cut_Man_t * p; - Abc_Obj_t * pObj; + Abc_Obj_t * pObj, * pNode; int i, nIters, fStatus; + Vec_Int_t * vChoices; int clk = clock(); assert( Abc_NtkIsSeq(pNtk) ); assert( pParams->fSeq ); +// assert( Abc_NtkIsDfsOrdered(pNtk) ); // start the manager pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); @@ -202,7 +204,10 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) if ( Abc_ObjFanoutNum(pObj) > 0 ) Cut_NodeSetTriv( p, pObj->Id ); Abc_NtkForEachPi( pNtk, pObj, i ) + { +//printf( "Setting trivial cut %d.\n", pObj->Id ); Cut_NodeSetTriv( p, pObj->Id ); + } // label the cutset nodes and set their number in the array // assign the elementary cuts to the cutset nodes Abc_SeqForEachCutsetNode( pNtk, pObj, i ) @@ -211,27 +216,40 @@ Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) pObj->fMarkC = 1; pObj->pCopy = (Abc_Obj_t *)i; Cut_NodeSetTriv( p, pObj->Id ); +//printf( "Setting trivial cut %d.\n", pObj->Id ); } // process the nodes + vChoices = Vec_IntAlloc( 100 ); for ( nIters = 0; nIters < 10; nIters++ ) { //printf( "ITERATION %d:\n", nIters ); // compute the cuts for the internal nodes Abc_AigForEachAnd( pNtk, pObj, i ) + { Abc_NodeGetCutsSeq( p, pObj, nIters==0 ); + // add cuts due to choices + if ( Abc_NodeIsAigChoice(pObj) ) + { + Vec_IntClear( vChoices ); + for ( pNode = pObj; pNode; pNode = pNode->pData ) + Vec_IntPush( vChoices, pNode->Id ); + Cut_NodeUnionCutsSeq( p, vChoices, (pObj->fMarkC ? (int)pObj->pCopy : -1), nIters==0 ); + } + } // merge the new cuts with the old cuts Abc_NtkForEachPi( pNtk, pObj, i ) Cut_NodeNewMergeWithOld( p, pObj->Id ); Abc_AigForEachAnd( pNtk, pObj, i ) Cut_NodeNewMergeWithOld( p, pObj->Id ); - // for the cutset, merge temp with new + // for the cutset, transfer temp cuts to new cuts fStatus = 0; Abc_SeqForEachCutsetNode( pNtk, pObj, i ) fStatus |= Cut_NodeTempTransferToNew( p, pObj->Id, i ); if ( fStatus == 0 ) break; } + Vec_IntFree( vChoices ); // if the status is not finished, transfer new to old for the cutset Abc_SeqForEachCutsetNode( pNtk, pObj, i ) diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index ac0d06be..bfc992ef 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -292,6 +292,7 @@ Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); } Extra_ProgressBarStop( pProgress ); + Abc_NtkReassignIds( pNtkNew ); return pNtkNew; } @@ -495,6 +496,7 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); Abc_NtkFraigTrustOne( pNtk, pNtkNew ); Abc_NtkFinalize( pNtk, pNtkNew ); + Abc_NtkReassignIds( pNtkNew ); // print a warning about choice nodes printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) ); diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index b06e7889..5c629b30 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -108,7 +108,7 @@ bool Abc_NtkFxuCheck( Abc_Ntk_t * pNtk ) { Abc_ObjForEachFanin( pNode, pFanin1, i ) { - if ( Abc_ObjFaninC(pNode, i) ) + if ( i < 2 && Abc_ObjFaninC(pNode, i) ) return 0; Abc_ObjForEachFanin( pNode, pFanin2, k ) { diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index fbc5e3ee..783585af 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -467,9 +467,9 @@ void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode ) pNode->pData = bFunc; // update the fanin order Abc_ObjForEachFanin( pNode, pFanin, i ) - pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ].iFan; + pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ]; Abc_ObjForEachFanin( pNode, pFanin, i ) - pNode->vFanins.pArray[i].iFan = pOrder[i]; + pNode->vFanins.pArray[i] = pOrder[i]; free( pOrder ); } diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 2bdd419d..e96825bb 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -58,7 +58,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pFile, " net = %5d", Abc_NtkNetNum(pNtk) ); fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); } - else if ( Abc_NtkIsStrash(pNtk) ) + else if ( Abc_NtkHasAig(pNtk) ) { fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); if ( Num = Abc_NtkGetChoiceNum(pNtk) ) @@ -66,8 +66,6 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) if ( Num = Abc_NtkGetExorNum(pNtk) ) fprintf( pFile, " (exor = %d)", Num ); } - else if ( Abc_NtkIsSeq(pNtk) ) - fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) ); else fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) ); diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 2b62d40f..9fe5bea0 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -607,7 +607,7 @@ void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 DdNode * bVar, * bTemp; int iFanin; assert( Abc_NtkIsBddLogic(pNode->pNtk) ); - if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 ) + if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 ) { printf( "Node %s should be among", Abc_ObjName(pFanin) ); printf( " the fanins of node %s...\n", Abc_ObjName(pNode) ); @@ -635,7 +635,7 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin ) DdNode * bVar, * bCof0, * bCof1; int iFanin; assert( Abc_NtkIsBddLogic(pNode->pNtk) ); - if ( (iFanin = Vec_FanFindEntry( &pNode->vFanins, pFanin->Id )) == -1 ) + if ( (iFanin = Vec_IntFind( &pNode->vFanins, pFanin->Id )) == -1 ) { printf( "Node %s should be among", Abc_ObjName(pFanin) ); printf( " the fanins of node %s...\n", Abc_ObjName(pNode) ); diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 7343582b..7bece42e 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -315,7 +315,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, fprintf( pFile, "Node%d%s", Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" ); - if ( Seq_ObjFaninL0(pNode) > 0 ) + if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL0(pNode) > 0 ) fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) ); fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); @@ -330,7 +330,7 @@ void Io_WriteDot( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, fprintf( pFile, "Node%d%s", Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") ); fprintf( pFile, " [" ); fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" ); - if ( Seq_ObjFaninL1(pNode) > 0 ) + if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL1(pNode) > 0 ) fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) ); fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); diff --git a/src/base/seq/module.make b/src/base/seq/module.make index 2bb176dc..fbb1015a 100644 --- a/src/base/seq/module.make +++ b/src/base/seq/module.make @@ -1,4 +1,6 @@ -SRC += src/base/seq/seqCreate.c \ +SRC += src/base/seq/seqAigCore.c \ + src/base/seq/seqAigIter.c \ + src/base/seq/seqCreate.c \ src/base/seq/seqFpgaCore.c \ src/base/seq/seqFpgaIter.c \ src/base/seq/seqLatch.c \ diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h index 2e1fef91..368f8afc 100644 --- a/src/base/seq/seq.h +++ b/src/base/seq/seq.h @@ -43,8 +43,16 @@ typedef struct Abc_Seq_t_ Abc_Seq_t; /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== seqAigCore.c ===========================================================*/ +extern void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ); +extern void Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ); +extern void Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ); /*=== seqFpgaCore.c ===============================================================*/ -extern Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose ); +extern Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose ); +/*=== seqMapCore.c ===============================================================*/ +extern Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose ); +/*=== seqRetCore.c ===========================================================*/ +extern Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose ); /*=== seqLatch.c ===============================================================*/ extern void Seq_NodeDupLats( Abc_Obj_t * pObjNew, Abc_Obj_t * pObj, int Edge ); extern int Seq_NodeCompareLats( Abc_Obj_t * pObj1, int Edge1, Abc_Obj_t * pObj2, int Edge2 ); @@ -57,10 +65,8 @@ extern Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ); /*=== seqShare.c =============================================================*/ extern void Seq_NtkShareFanouts( Abc_Ntk_t * pNtk ); -/*=== seqRetCore.c ===========================================================*/ -extern void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ); -extern void Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ); -extern void Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ); +extern void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk ); +extern void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds ); /*=== seqUtil.c ==============================================================*/ extern char * Seq_ObjFaninGetInitPrintable( Abc_Obj_t * pObj, int Edge ); extern void Seq_NtkLatchSetValues( Abc_Ntk_t * pNtk, Abc_InitType_t Init ); @@ -69,6 +75,7 @@ extern int Seq_NtkLatchNumMax( Abc_Ntk_t * pNtk ); extern int Seq_NtkLatchNumShared( Abc_Ntk_t * pNtk ); extern void Seq_NtkLatchGetInitNums( Abc_Ntk_t * pNtk, int * pInits ); extern int Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk ); +extern int Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c new file mode 100644 index 00000000..d347d53e --- /dev/null +++ b/src/base/seq/seqAigCore.c @@ -0,0 +1,970 @@ +/**CFile**************************************************************** + + FileName [seqRetCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Construction and manipulation of sequential AIGs.] + + Synopsis [The core of retiming procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: seqRetCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "seqInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + Retiming can be represented in three equivalent forms: + - as a set of integer lags for each node (array of chars by node ID) + - as a set of node numbers with lag for each, fwd and bwd (two arrays of Seq_RetStep_t_) + - as a set of latch moves over the nodes, fwd and bwd (two arrays of node pointers Abc_Obj_t *) +*/ + +static void Abc_ObjRetimeForward( Abc_Obj_t * pObj ); +static int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues ); +static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ); +static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ); + +static void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ); +static int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose ); +static void Abc_ObjRetimeForward( Abc_Obj_t * pObj ); +static int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues ); +static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ); +static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ); + +static Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward ); +static Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward ); +static Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward ); +static void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches ); +static void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs performs optimal delay retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + int RetValue; + if ( !fInitial ) + Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC ); + // get the retiming lags + Seq_AigRetimeDelayLags( pNtk, fVerbose ); + // implement this retiming + RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose ); + if ( RetValue == 0 ) + printf( "Retiming completed but initial state computation has failed.\n" ); +} + +/**Function************************************************************* + + Synopsis [Performs most forward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ) +{ + Vec_Ptr_t * vMoves; + Abc_Obj_t * pNode; + int i; + if ( !fInitial ) + Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC ); + // get the forward moves + vMoves = Abc_NtkUtilRetimingTry( pNtk, 1 ); + // undo the forward moves + Vec_PtrForEachEntryReverse( vMoves, pNode, i ) + Abc_ObjRetimeBackwardTry( pNode, 1 ); + // implement this forward retiming + Seq_NtkImplementRetimingForward( pNtk, vMoves ); + Vec_PtrFree( vMoves ); +} + +/**Function************************************************************* + + Synopsis [Performs most backward retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ) +{ + Vec_Ptr_t * vMoves; + Abc_Obj_t * pNode; + int i, RetValue; + if ( !fInitial ) + Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC ); + // get the backward moves + vMoves = Abc_NtkUtilRetimingTry( pNtk, 0 ); + // undo the backward moves + Vec_PtrForEachEntryReverse( vMoves, pNode, i ) + Abc_ObjRetimeForwardTry( pNode, 1 ); + // implement this backward retiming + RetValue = Seq_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose ); + Vec_PtrFree( vMoves ); + if ( RetValue == 0 ) + printf( "Retiming completed but initial state computation has failed.\n" ); +} + + + + +/**Function************************************************************* + + Synopsis [Implements the retiming on the sequential AIG.] + + Description [Split the retiming into forward and backward.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose ) +{ + Vec_Int_t * vSteps; + Vec_Ptr_t * vMoves; + int RetValue; + + // forward retiming + vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 ); + // translate each set of steps into moves + if ( fVerbose ) + printf( "The number of forward steps = %6d.\n", Vec_IntSize(vSteps) ); + vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 ); + if ( fVerbose ) + printf( "The number of forward moves = %6d.\n", Vec_PtrSize(vMoves) ); + // implement this retiming + Seq_NtkImplementRetimingForward( pNtk, vMoves ); + Vec_IntFree( vSteps ); + Vec_PtrFree( vMoves ); + + // backward retiming + vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 ); + // translate each set of steps into moves + if ( fVerbose ) + printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) ); + vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 ); + if ( fVerbose ) + printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) ); + // implement this retiming + RetValue = Seq_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose ); + Vec_IntFree( vSteps ); + Vec_PtrFree( vMoves ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Implements the given retiming on the sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) +{ + Abc_Obj_t * pNode; + int i; + Vec_PtrForEachEntry( vMoves, pNode, i ) + Abc_ObjRetimeForward( pNode ); +} + +/**Function************************************************************* + + Synopsis [Retimes node forward by one latch.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRetimeForward( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanout; + int Init0, Init1, Init, i; + assert( Abc_ObjFaninNum(pObj) == 2 ); + assert( Seq_ObjFaninL0(pObj) >= 1 ); + assert( Seq_ObjFaninL1(pObj) >= 1 ); + // remove the init values from the fanins + Init0 = Seq_NodeDeleteFirst( pObj, 0 ); + Init1 = Seq_NodeDeleteFirst( pObj, 1 ); + assert( Init0 != ABC_INIT_NONE ); + assert( Init1 != ABC_INIT_NONE ); + // take into account the complements in the node + if ( Abc_ObjFaninC0(pObj) ) + { + if ( Init0 == ABC_INIT_ZERO ) + Init0 = ABC_INIT_ONE; + else if ( Init0 == ABC_INIT_ONE ) + Init0 = ABC_INIT_ZERO; + } + if ( Abc_ObjFaninC1(pObj) ) + { + if ( Init1 == ABC_INIT_ZERO ) + Init1 = ABC_INIT_ONE; + else if ( Init1 == ABC_INIT_ONE ) + Init1 = ABC_INIT_ZERO; + } + // compute the value at the output of the node + if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO ) + Init = ABC_INIT_ZERO; + else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE ) + Init = ABC_INIT_ONE; + else + Init = ABC_INIT_DC; + + // make sure the label is clean + Abc_ObjForEachFanout( pObj, pFanout, i ) + assert( pFanout->fMarkC == 0 ); + // add the init values to the fanouts + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( pFanout->fMarkC ) + continue; + pFanout->fMarkC = 1; + if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) ) + Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init ); + else + { + assert( Abc_ObjFanin0(pFanout) == pObj ); + Seq_NodeInsertLast( pFanout, 0, Init ); + Seq_NodeInsertLast( pFanout, 1, Init ); + } + } + // clean the label + Abc_ObjForEachFanout( pObj, pFanout, i ) + pFanout->fMarkC = 0; +} + + +/**Function************************************************************* + + Synopsis [Implements the given retiming on the sequential AIG.] + + Description [Returns 0 of initial state computation fails.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose ) +{ + Seq_RetEdge_t RetEdge; + stmm_table * tTable; + stmm_generator * gen; + Vec_Int_t * vValues; + Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf; + Abc_Obj_t * pNode, * pNodeNew; + int * pModel, RetValue, i, clk; + + // return if the retiming is trivial + if ( Vec_PtrSize(vMoves) == 0 ) + return 1; + + // create the network for the initial state computation + // start the table and the array of PO values + pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); + tTable = stmm_init_table( stmm_numcmp, stmm_numhash ); + vValues = Vec_IntAlloc( 100 ); + + // perform the backward moves and build the network for initial state computation + RetValue = 0; + Vec_PtrForEachEntry( vMoves, pNode, i ) + RetValue |= Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues ); + + // add the PIs corresponding to the white spots + stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew ) + Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) ); + + // add the PI/PO names + Abc_NtkAddDummyPiNames( pNtkProb ); + Abc_NtkAddDummyPoNames( pNtkProb ); + + // make sure everything is okay with the network structure + if ( !Abc_NtkDoCheck( pNtkProb ) ) + { + printf( "Seq_NtkImplementRetimingBackward: The internal network check has failed.\n" ); + Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); + Abc_NtkDelete( pNtkProb ); + stmm_free_table( tTable ); + Vec_IntFree( vValues ); + return 0; + } + + // check if conflict is found + if ( RetValue ) + { + printf( "Seq_NtkImplementRetimingBackward: A top level conflict is detected. DC latch values are used.\n" ); + Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); + Abc_NtkDelete( pNtkProb ); + stmm_free_table( tTable ); + Vec_IntFree( vValues ); + return 0; + } + + // get the miter cone + pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues ); + Abc_NtkDelete( pNtkProb ); + Vec_IntFree( vValues ); + + if ( fVerbose ) + printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) ); + + // transform the miter into a logic network for efficient CNF construction + pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 ); + Abc_NtkDelete( pNtkMiter ); + + // solve the miter +clk = clock(); + RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 ); +if ( fVerbose ) +if ( clock() - clk > 100 ) +{ +PRT( "SAT solving time", clock() - clk ); +} + pModel = pNtkCnf->pModel; pNtkCnf->pModel = NULL; + Abc_NtkDelete( pNtkCnf ); + + // analyze the result + if ( RetValue == -1 || RetValue == 1 ) + { + Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); + if ( RetValue == 1 ) + printf( "Seq_NtkImplementRetimingBackward: The problem is unsatisfiable. DC latch values are used.\n" ); + else + printf( "Seq_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" ); + stmm_free_table( tTable ); + return 0; + } + + // set the values of the latches + Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel ); + stmm_free_table( tTable ); + free( pModel ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Retimes node backward by one latch.] + + Description [Constructs the problem for initial state computation. + Returns 1 if the conflict is found.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * tTable, Vec_Int_t * vValues ) +{ + Abc_Obj_t * pFanout; + Abc_InitType_t Init, Value; + Seq_RetEdge_t RetEdge; + Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuffer; + int i, Edge, fMet0, fMet1, fMetN; + + // make sure the node can be retimed + assert( Seq_ObjFanoutLMin(pObj) > 0 ); + // get the fanout values + fMet0 = fMet1 = fMetN = 0; + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( Abc_ObjFaninId0(pFanout) == pObj->Id ) + { + Init = Seq_NodeGetInitLast( pFanout, 0 ); + if ( Init == ABC_INIT_ZERO ) + fMet0 = 1; + else if ( Init == ABC_INIT_ONE ) + fMet1 = 1; + else if ( Init == ABC_INIT_NONE ) + fMetN = 1; + } + if ( Abc_ObjFaninId1(pFanout) == pObj->Id ) + { + Init = Seq_NodeGetInitLast( pFanout, 1 ); + if ( Init == ABC_INIT_ZERO ) + fMet0 = 1; + else if ( Init == ABC_INIT_ONE ) + fMet1 = 1; + else if ( Init == ABC_INIT_NONE ) + fMetN = 1; + } + } + + // consider the case when all fanout latches have don't-care values + // the new values on the fanin edges will be don't-cares + if ( !fMet0 && !fMet1 && !fMetN ) + { + // make sure the label is clean + Abc_ObjForEachFanout( pObj, pFanout, i ) + assert( pFanout->fMarkC == 0 ); + // update the fanout edges + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( pFanout->fMarkC ) + continue; + pFanout->fMarkC = 1; + if ( Abc_ObjFaninId0(pFanout) == pObj->Id ) + Seq_NodeDeleteLast( pFanout, 0 ); + if ( Abc_ObjFaninId1(pFanout) == pObj->Id ) + Seq_NodeDeleteLast( pFanout, 1 ); + } + // clean the label + Abc_ObjForEachFanout( pObj, pFanout, i ) + pFanout->fMarkC = 0; + // update the fanin edges + Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable ); + Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable ); + Seq_NodeInsertFirst( pObj, 0, ABC_INIT_DC ); + Seq_NodeInsertFirst( pObj, 1, ABC_INIT_DC ); + return 0; + } + // the initial values on the fanout edges contain 0, 1, or unknown + // the new values on the fanin edges will be unknown + + // add new AND-gate to the network + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + + // add PO fanouts if any + if ( fMet0 ) + { + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); + Vec_IntPush( vValues, 0 ); + } + if ( fMet1 ) + { + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); + Vec_IntPush( vValues, 1 ); + } + + // make sure the label is clean + Abc_ObjForEachFanout( pObj, pFanout, i ) + assert( pFanout->fMarkC == 0 ); + // perform the changes + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( pFanout->fMarkC ) + continue; + pFanout->fMarkC = 1; + if ( Abc_ObjFaninId0(pFanout) == pObj->Id ) + { + Edge = 0; + Value = Seq_NodeDeleteLast( pFanout, Edge ); + if ( Value != ABC_INIT_NONE ) + continue; + // value is unknown, remove it from the table + RetEdge.iNode = pFanout->Id; + RetEdge.iEdge = Edge; + RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed + if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) + assert( 0 ); + // create the fanout of the AND gate + Abc_ObjAddFanin( pFanoutNew, pNodeNew ); + } + if ( Abc_ObjFaninId1(pFanout) == pObj->Id ) + { + Edge = 1; + Value = Seq_NodeDeleteLast( pFanout, Edge ); + if ( Value != ABC_INIT_NONE ) + continue; + // value is unknown, remove it from the table + RetEdge.iNode = pFanout->Id; + RetEdge.iEdge = Edge; + RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed + if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) + assert( 0 ); + // create the fanout of the AND gate + Abc_ObjAddFanin( pFanoutNew, pNodeNew ); + } + } + // clean the label + Abc_ObjForEachFanout( pObj, pFanout, i ) + pFanout->fMarkC = 0; + + // update the fanin edges + Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable ); + Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable ); + Seq_NodeInsertFirst( pObj, 0, ABC_INIT_NONE ); + Seq_NodeInsertFirst( pObj, 1, ABC_INIT_NONE ); + + // add the buffer + pBuffer = Abc_NtkCreateNode( pNtkNew ); + pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); + Abc_ObjAddFanin( pNodeNew, pBuffer ); + // point to it from the table + RetEdge.iNode = pObj->Id; + RetEdge.iEdge = 0; + RetEdge.iLatch = 0; + if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) ) + assert( 0 ); + + // add the buffer + pBuffer = Abc_NtkCreateNode( pNtkNew ); + pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); + Abc_ObjAddFanin( pNodeNew, pBuffer ); + // point to it from the table + RetEdge.iNode = pObj->Id; + RetEdge.iEdge = 1; + RetEdge.iLatch = 0; + if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) ) + assert( 0 ); + + // report conflict is found + return fMet0 && fMet1; +} + +/**Function************************************************************* + + Synopsis [Generates the printable edge label with the initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ) +{ + Abc_Obj_t * pFanoutNew; + Seq_RetEdge_t RetEdge; + Abc_InitType_t Init; + int nLatches, i; + + // get the number of latches on the edge + nLatches = Seq_ObjFaninL( pObj, Edge ); + for ( i = nLatches - 1; i >= 0; i-- ) + { + // get the value of this latch + Init = Seq_NodeGetInitOne( pObj, Edge, i ); + if ( Init != ABC_INIT_NONE ) + continue; + // get the retiming edge + RetEdge.iNode = pObj->Id; + RetEdge.iEdge = Edge; + RetEdge.iLatch = i; + // remove entry from table and add it with a different key + if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) + assert( 0 ); + RetEdge.iLatch++; + if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pFanoutNew ) ) + assert( 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Sets the initial values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ) +{ + Abc_Obj_t * pNode; + stmm_generator * gen; + Seq_RetEdge_t RetEdge; + Abc_InitType_t Init; + int i; + + i = 0; + stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL ) + { + pNode = Abc_NtkObj( pNtk, RetEdge.iNode ); + Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC; + Seq_NodeSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init ); + i++; + } +} + + + +/**Function************************************************************* + + Synopsis [Performs forward retiming of the sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward ) +{ + Vec_Ptr_t * vNodes, * vMoves; + Abc_Obj_t * pNode, * pFanout, * pFanin; + int i, k, nLatches; + assert( Abc_NtkIsSeq( pNtk ) ); + // assume that all nodes can be retimed + vNodes = Vec_PtrAlloc( 100 ); + Abc_AigForEachAnd( pNtk, pNode, i ) + { + Vec_PtrPush( vNodes, pNode ); + pNode->fMarkA = 1; + } + // process the nodes + vMoves = Vec_PtrAlloc( 100 ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { +// printf( "(%d,%d) ", Seq_ObjFaninL0(pNode), Seq_ObjFaninL0(pNode) ); + // unmark the node as processed + pNode->fMarkA = 0; + // get the number of latches to retime + if ( fForward ) + nLatches = Seq_ObjFaninLMin(pNode); + else + nLatches = Seq_ObjFanoutLMin(pNode); + if ( nLatches == 0 ) + continue; + assert( nLatches > 0 ); + // retime the latches forward + if ( fForward ) + Abc_ObjRetimeForwardTry( pNode, nLatches ); + else + Abc_ObjRetimeBackwardTry( pNode, nLatches ); + // write the moves + for ( k = 0; k < nLatches; k++ ) + Vec_PtrPush( vMoves, pNode ); + // schedule fanouts for updating + if ( fForward ) + { + Abc_ObjForEachFanout( pNode, pFanout, k ) + { + if ( Abc_ObjFaninNum(pFanout) != 2 || pFanout->fMarkA ) + continue; + pFanout->fMarkA = 1; + Vec_PtrPush( vNodes, pFanout ); + } + } + else + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + if ( Abc_ObjFaninNum(pFanin) != 2 || pFanin->fMarkA ) + continue; + pFanin->fMarkA = 1; + Vec_PtrPush( vNodes, pFanin ); + } + } + } + Vec_PtrFree( vNodes ); + // make sure the marks are clean the the retiming is final + Abc_AigForEachAnd( pNtk, pNode, i ) + { + assert( pNode->fMarkA == 0 ); + if ( fForward ) + assert( Seq_ObjFaninLMin(pNode) == 0 ); + else + assert( Seq_ObjFanoutLMin(pNode) == 0 ); + } + return vMoves; +} + +/**Function************************************************************* + + Synopsis [Translates retiming steps into retiming moves.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward ) +{ + Seq_RetStep_t RetStep; + Vec_Ptr_t * vMoves; + Abc_Obj_t * pNode; + int i, k, iNode, nLatches, Number; + int fChange; + assert( Abc_NtkIsSeq( pNtk ) ); + +/* + // try implementing all the moves at once + Vec_IntForEachEntry( vSteps, Number, i ) + { + // get the retiming step + RetStep = Seq_Int2RetStep( Number ); + // get the node to be retimed + pNode = Abc_NtkObj( pNtk, RetStep.iNode ); + assert( RetStep.nLatches > 0 ); + nLatches = RetStep.nLatches; + + if ( fForward ) + Abc_ObjRetimeForwardTry( pNode, nLatches ); + else + Abc_ObjRetimeBackwardTry( pNode, nLatches ); + } + // now look if any node has wrong number of latches + Abc_AigForEachAnd( pNtk, pNode, i ) + { + if ( Seq_ObjFaninL0(pNode) < 0 ) + printf( "Wrong 0node %d.\n", pNode->Id ); + if ( Seq_ObjFaninL1(pNode) < 0 ) + printf( "Wrong 1node %d.\n", pNode->Id ); + } + // try implementing all the moves at once + Vec_IntForEachEntry( vSteps, Number, i ) + { + // get the retiming step + RetStep = Seq_Int2RetStep( Number ); + // get the node to be retimed + pNode = Abc_NtkObj( pNtk, RetStep.iNode ); + assert( RetStep.nLatches > 0 ); + nLatches = RetStep.nLatches; + + if ( !fForward ) + Abc_ObjRetimeForwardTry( pNode, nLatches ); + else + Abc_ObjRetimeBackwardTry( pNode, nLatches ); + } +*/ + + // process the nodes + vMoves = Vec_PtrAlloc( 100 ); + while ( Vec_IntSize(vSteps) > 0 ) + { + iNode = 0; + fChange = 0; + Vec_IntForEachEntry( vSteps, Number, i ) + { + // get the retiming step + RetStep = Seq_Int2RetStep( Number ); + // get the node to be retimed + pNode = Abc_NtkObj( pNtk, RetStep.iNode ); + assert( RetStep.nLatches > 0 ); + // get the number of latches that can be retimed + if ( fForward ) + nLatches = Seq_ObjFaninLMin(pNode); + else + nLatches = Seq_ObjFanoutLMin(pNode); + if ( nLatches == 0 ) + { + Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) ); + continue; + } + assert( nLatches > 0 ); + fChange = 1; + // get the number of latches to be retimed over this node + nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches ); + // retime the latches forward + if ( fForward ) + Abc_ObjRetimeForwardTry( pNode, nLatches ); + else + Abc_ObjRetimeBackwardTry( pNode, nLatches ); + // write the moves + for ( k = 0; k < nLatches; k++ ) + Vec_PtrPush( vMoves, pNode ); + // subtract the retiming performed + RetStep.nLatches -= nLatches; + // store the node if it is not retimed completely + if ( RetStep.nLatches > 0 ) + Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) ); + } + // reduce the array + Vec_IntShrink( vSteps, iNode ); + if ( !fChange ) + { + printf( "Warning: %d strange steps (a minor bug to be fixed later).\n", Vec_IntSize(vSteps) ); +/* + Vec_IntForEachEntry( vSteps, Number, i ) + { + RetStep = Seq_Int2RetStep( Number ); + printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches ); + } + printf( "\n" ); +*/ + break; + } + } + // undo the tentative retiming + if ( fForward ) + { + Vec_PtrForEachEntryReverse( vMoves, pNode, i ) + Abc_ObjRetimeBackwardTry( pNode, 1 ); + } + else + { + Vec_PtrForEachEntryReverse( vMoves, pNode, i ) + Abc_ObjRetimeForwardTry( pNode, 1 ); + } + return vMoves; +} + + +/**Function************************************************************* + + Synopsis [Splits retiming into forward and backward.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward ) +{ + Vec_Int_t * vNodes; + Seq_RetStep_t RetStep; + int Value, i; + vNodes = Vec_IntAlloc( 100 ); + Vec_StrForEachEntry( vLags, Value, i ) + { + if ( Value < 0 && fForward ) + { + RetStep.iNode = i; + RetStep.nLatches = -Value; + Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) ); + } + else if ( Value > 0 && !fForward ) + { + RetStep.iNode = i; + RetStep.nLatches = Value; + Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) ); + } + } + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Retime node forward without initial states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches ) +{ + Abc_Obj_t * pFanout; + int i; + // make sure it is an AND gate + assert( Abc_ObjFaninNum(pObj) == 2 ); + // make sure it has enough latches +// assert( Seq_ObjFaninL0(pObj) >= nLatches ); +// assert( Seq_ObjFaninL1(pObj) >= nLatches ); + // subtract these latches on the fanin side + Seq_ObjAddFaninL0( pObj, -nLatches ); + Seq_ObjAddFaninL1( pObj, -nLatches ); + // make sure the label is clean + Abc_ObjForEachFanout( pObj, pFanout, i ) + assert( pFanout->fMarkC == 0 ); + // add these latches on the fanout side + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( pFanout->fMarkC ) + continue; + pFanout->fMarkC = 1; + if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) ) + Seq_ObjAddFanoutL( pObj, pFanout, nLatches ); + else + { + assert( Abc_ObjFanin0(pFanout) == pObj ); + Seq_ObjAddFaninL0( pFanout, nLatches ); + Seq_ObjAddFaninL1( pFanout, nLatches ); + } + } + // clean the label + Abc_ObjForEachFanout( pObj, pFanout, i ) + pFanout->fMarkC = 0; +} + +/**Function************************************************************* + + Synopsis [Retime node backward without initial states.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches ) +{ + Abc_Obj_t * pFanout; + int i; + // make sure it is an AND gate + assert( Abc_ObjFaninNum(pObj) == 2 ); + // make sure the label is clean + Abc_ObjForEachFanout( pObj, pFanout, i ) + assert( pFanout->fMarkC == 0 ); + // subtract these latches on the fanout side + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( pFanout->fMarkC ) + continue; + pFanout->fMarkC = 1; +// assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches ); + if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) ) + Seq_ObjAddFanoutL( pObj, pFanout, -nLatches ); + else + { + assert( Abc_ObjFanin0(pFanout) == pObj ); + Seq_ObjAddFaninL0( pFanout, -nLatches ); + Seq_ObjAddFaninL1( pFanout, -nLatches ); + } + } + // clean the label + Abc_ObjForEachFanout( pObj, pFanout, i ) + pFanout->fMarkC = 0; + // add these latches on the fanin side + Seq_ObjAddFaninL0( pObj, nLatches ); + Seq_ObjAddFaninL1( pObj, nLatches ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/seq/seqAigIter.c b/src/base/seq/seqAigIter.c new file mode 100644 index 00000000..9b423d32 --- /dev/null +++ b/src/base/seq/seqAigIter.c @@ -0,0 +1,245 @@ +/**CFile**************************************************************** + + FileName [seqRetIter.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Construction and manipulation of sequential AIGs.] + + Synopsis [The iterative L-Value computation for retiming procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: seqRetIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "seqInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// the internal procedures +static int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose ); +static int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose ); +static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Retimes AIG for optimal delay using Pan's algorithm.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Abc_Obj_t * pNode; + int i, FiMax, FiBest, RetValue; + char NodeLag; + + assert( Abc_NtkIsSeq( pNtk ) ); + + // get the upper bound on the clock period + FiMax = 2 + Seq_NtkLevelMax(pNtk); + + // make sure this clock period is feasible + assert( Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) ); + + // search for the optimal clock period between 0 and nLevelMax + FiBest = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose ); + + // recompute the best l-values + RetValue = Seq_RetimeForPeriod( pNtk, FiBest, fVerbose ); + assert( RetValue ); + + // write the retiming lags + Vec_StrFill( p->vLags, p->nSize, 0 ); + Abc_AigForEachAnd( pNtk, pNode, i ) + { + NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest ); + Seq_NodeSetLag( pNode, NodeLag ); + } +/* + { + Abc_Obj_t * pFanin, * pFanout; + pNode = Abc_NtkObj( pNtk, 823 ); + printf( "Node %d. Lag = %d. LValue = %d. Latches = (%d,%d) (%d,%d).\n", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLValue(pNode), + Seq_ObjFaninL0(pNode), Seq_ObjFaninL1(pNode), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 826)), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 1210)) ); + pFanin = Abc_ObjFanin0( pNode ); + printf( "Fanin %d. Lag = %d. LValue = %d. Latches = (%d,%d)\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin), + Seq_ObjFaninL0(pFanin), Seq_ObjFaninL1(pFanin) ); + pFanin = Abc_ObjFanin1( pNode ); + printf( "Fanin %d. Lag = %d. LValue = %d.\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin) ); + Abc_ObjForEachFanout( pNode, pFanout, i ) + printf( "Fanout %d. Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) ); + Abc_ObjForEachFanout( Abc_ObjFanin0(pNode), pFanout, i ) + printf( "Fanout %d. Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) ); + } +*/ + + // print the result + if ( fVerbose ) + printf( "The best clock period is %3d.\n", FiBest ); + +/* + printf( "LValues : " ); + Abc_AigForEachAnd( pNtk, pNode, i ) + printf( "%d=%d ", i, Seq_NodeGetLValue(pNode) ); + printf( "\n" ); + printf( "Lags : " ); + Abc_AigForEachAnd( pNtk, pNode, i ) + if ( Vec_StrEntry(p->vLags,i) != 0 ) + printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(p->vLags,i), Seq_NodeGetLValue(pNode), Seq_NodeGetLValue(pNode) - FiBest * Vec_StrEntry(p->vLags,i) ); + printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Performs binary search for the optimal clock period.] + + Description [Assumes that FiMin is infeasible while FiMax is feasible.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose ) +{ + int Median; + assert( FiMin < FiMax ); + if ( FiMin + 1 == FiMax ) + return FiMax; + Median = FiMin + (FiMax - FiMin)/2; + if ( Seq_RetimeForPeriod( pNtk, Median, fVerbose ) ) + return Seq_RetimeSearch_rec( pNtk, FiMin, Median, fVerbose ); // Median is feasible + else + return Seq_RetimeSearch_rec( pNtk, Median, FiMax, fVerbose ); // Median is infeasible +} + +/**Function************************************************************* + + Synopsis [Returns 1 if retiming with this clock period is feasible.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Abc_Obj_t * pObj; + int i, c, RetValue, fChange, Counter; + char * pReason = ""; + + // set l-values of all nodes to be minus infinity + Vec_IntFill( p->vLValues, p->nSize, -ABC_INFINITY ); + + // set l-values of constants and PIs + pObj = Abc_NtkObj( pNtk, 0 ); + Seq_NodeSetLValue( pObj, 0 ); + Abc_NtkForEachPi( pNtk, pObj, i ) + Seq_NodeSetLValue( pObj, 0 ); + + // update all values iteratively + Counter = 0; + for ( c = 0; c < p->nMaxIters; c++ ) + { + fChange = 0; + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Counter++; + if ( Seq_NodeCutMan(pObj) ) + RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi ); + else + RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi ); + if ( RetValue == SEQ_UPDATE_YES ) + fChange = 1; + } + Abc_NtkForEachPo( pNtk, pObj, i ) + { + if ( Seq_NodeCutMan(pObj) ) + RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi ); + else + RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi ); + if ( RetValue == SEQ_UPDATE_FAIL ) + break; + } + if ( RetValue == SEQ_UPDATE_FAIL ) + break; + if ( fChange == 0 ) + break; + } + if ( c == p->nMaxIters ) + { + RetValue = SEQ_UPDATE_FAIL; + pReason = "(timeout)"; + } + else + c++; + // report the results + if ( fVerbose ) + { + if ( RetValue == SEQ_UPDATE_FAIL ) + printf( "Period = %3d. Iterations = %3d. Updates = %10d. Infeasible %s\n", Fi, c, Counter, pReason ); + else + printf( "Period = %3d. Iterations = %3d. Updates = %10d. Feasible\n", Fi, c, Counter ); + } + return RetValue != SEQ_UPDATE_FAIL; +} + +/**Function************************************************************* + + Synopsis [Computes the l-value of the node.] + + Description [The node can be internal or a PO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ) +{ + int lValueNew, lValueOld, lValue0, lValue1; + assert( !Abc_ObjIsPi(pObj) ); + assert( Abc_ObjFaninNum(pObj) > 0 ); + lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj); + if ( Abc_ObjIsPo(pObj) ) + return (lValue0 > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO; + if ( Abc_ObjFaninNum(pObj) == 2 ) + lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Seq_ObjFaninL1(pObj); + else + lValue1 = -ABC_INFINITY; + lValueNew = 1 + ABC_MAX( lValue0, lValue1 ); + lValueOld = Seq_NodeGetLValue(pObj); +// if ( lValueNew == lValueOld ) + if ( lValueNew <= lValueOld ) + return SEQ_UPDATE_NO; + Seq_NodeSetLValue( pObj, lValueNew ); + return SEQ_UPDATE_YES; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c index 05eebe15..d293b946 100644 --- a/src/base/seq/seqCreate.c +++ b/src/base/seq/seqCreate.c @@ -75,13 +75,16 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj, * pFaninNew; Vec_Int_t * vInitValues; Abc_InitType_t Init; - int i, k; + int i, k, RetValue; // make sure it is an AIG without self-feeding latches assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); assert( Abc_NtkIsDfsOrdered(pNtk) ); + if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) ) + printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); + assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); + // start the network pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG ); // duplicate the name and the spec @@ -235,7 +238,6 @@ void Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk ) } } - /**Function************************************************************* Synopsis [Converts a sequential AIG into a logic SOP network.] @@ -251,6 +253,76 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; Abc_Obj_t * pObj, * pObjNew, * pFaninNew; + Seq_Lat_t * pRing; + int i; + + assert( Abc_NtkIsSeq(pNtk) ); + // start the network without latches + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // duplicate the nodes + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Abc_NtkDupObj(pNtkNew, pObj); + pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + } + // share and create the latches + Seq_NtkShareLatches( pNtkNew, pNtk ); + // connect the objects + Abc_AigForEachAnd( pNtk, pObj, i ) + { + if ( pRing = Seq_NodeGetRing(pObj,0) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin0(pObj)->pCopy; + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + + if ( pRing = Seq_NodeGetRing(pObj,1) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin1(pObj)->pCopy; + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + } + // connect the POs + Abc_NtkForEachPo( pNtk, pObj, i ) + { + if ( pRing = Seq_NodeGetRing(pObj,0) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin0(pObj)->pCopy; + pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + } + + // add the latches and their names + Abc_NtkAddDummyLatchNames( pNtkNew ); + Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) + { + Vec_PtrPush( pNtkNew->vCis, pObjNew ); + Vec_PtrPush( pNtkNew->vCos, pObjNew ); + } + // fix the problem with complemented and duplicated CO edges + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Converts a sequential AIG into a logic SOP network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pObjNew, * pFaninNew; int i; assert( Abc_NtkIsSeq(pNtk) ); diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c index cb000ab9..030efd80 100644 --- a/src/base/seq/seqFpgaCore.c +++ b/src/base/seq/seqFpgaCore.c @@ -29,9 +29,11 @@ static int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose ); static Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtkNew ); static int Seq_FpgaMappingCount( Abc_Ntk_t * pNtk ); static int Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves ); +static Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves ); static DdNode * Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves ); static void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges ); -static Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves ); +static void Seq_FpgaMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); +static DdNode * Seq_FpgaMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -48,13 +50,25 @@ static Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * p SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose ) +Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose ) { + Abc_Seq_t * p = pNtk->pManFunc; Abc_Ntk_t * pNtkNew; Abc_Ntk_t * pNtkMap; int RetValue; + + // get the LUT library + p->nVarsMax = Fpga_LutLibReadVarMax( Abc_FrameReadLibLut() ); + p->nMaxIters = nMaxIters; + // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags) Seq_FpgaMappingDelays( pNtk, fVerbose ); + if ( RetValue = Abc_NtkGetChoiceNum(pNtk) ) + { + printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue ); + return NULL; + } + // duplicate the nodes contained in multiple cuts pNtkNew = Seq_NtkFpgaDup( pNtk ); // return pNtkNew; @@ -67,14 +81,13 @@ Abc_Ntk_t * Seq_NtkFpgaMapRetime( Abc_Ntk_t * pNtk, int fVerbose ) // check the compatibility of initial states computed if ( RetValue = Seq_NtkFpgaInitCompatible( pNtkNew, fVerbose ) ) - { printf( "The number of LUTs with incompatible edges = %d.\n", RetValue ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } // create the final mapped network pNtkMap = Seq_NtkSeqFpgaMapped( pNtkNew ); Abc_NtkDelete( pNtkNew ); + if ( RetValue ) + printf( "The number of LUTs with more than %d inputs = %d.\n", + p->nVarsMax, Seq_NtkCountNodesAboveLimit(pNtkMap, p->nVarsMax) ); return pNtkMap; } @@ -125,7 +138,6 @@ Abc_Ntk_t * Seq_NtkFpgaDup( Abc_Ntk_t * pNtk ) // duplicate the latches on the PO edges Abc_NtkForEachPo( pNtk, pObj, i ) Seq_NodeDupLats( pObj->pCopy, pObj, 0 ); -//Abc_NtkShowAig( pNtkNew ); // transfer the mapping info to the new manager Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) @@ -264,13 +276,11 @@ int Seq_NtkFpgaInitCompatible( Abc_Ntk_t * pNtk, int fVerbose ) Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk ) { Abc_Seq_t * p = pNtk->pManFunc; - Seq_Lat_t * pLat, * pRing; Abc_Ntk_t * pNtkMap; - Vec_Vec_t * vTotalEdges; - Vec_Ptr_t * vLeaves, * vMapEdges; - Abc_Obj_t * pObj, * pAnd, * pLeaf, * pFanout, * pFanin, * pLatch; - int i, k, m, Edge, nLatches, nLatchAfter; - unsigned SeqEdge; + Vec_Ptr_t * vLeaves; + Abc_Obj_t * pObj, * pLatch, * pFaninNew; + Seq_Lat_t * pRing; + int i; assert( Abc_NtkIsSeq(pNtk) ); @@ -278,87 +288,33 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk ) pNtkMap = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); // duplicate the nodes used in the mapping - Vec_PtrForEachEntry( p->vMapAnds, pAnd, i ) - { - pAnd->pCopy = Abc_NtkCreateNode( pNtkMap ); - // get the leaves of this gate - vLeaves = Vec_VecEntry( p->vMapCuts, i ); - // get the BDD of the node - pAnd->pCopy->pData = Seq_FpgaMappingBdd_rec( pNtkMap->pManFunc, pNtk, pAnd->Id << 8, vLeaves ); - Cudd_Ref( pAnd->pCopy->pData ); - } + Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) + pObj->pCopy = Abc_NtkCreateNode( pNtkMap ); + // create and share the latches + Seq_NtkShareLatchesFpga( pNtkMap, pNtk, p->vMapAnds ); - // construct nodes in the mapped network - vTotalEdges = Vec_VecStart( p->nVarsMax ); - Vec_PtrForEachEntry( p->vMapAnds, pAnd, i ) + // connect the nodes + Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) { // get the leaves of this gate vLeaves = Vec_VecEntry( p->vMapCuts, i ); - // get the edges pointing to the leaves - Vec_VecClear( vTotalEdges ); - Seq_FpgaMappingEdges_rec( pNtk, pAnd->Id << 8, NULL, vLeaves, vTotalEdges ); - // for each leaf, consider its edges - Vec_PtrForEachEntry( vLeaves, pLeaf, k ) - { - SeqEdge = (unsigned)pLeaf; - pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 ); - nLatchAfter = SeqEdge & 255; - if ( nLatchAfter == 0 ) - { - // add the fanin - Abc_ObjAddFanin( pAnd->pCopy, pLeaf->pCopy ); - continue; - } - - // get the first edge - vMapEdges = Vec_VecEntry( vTotalEdges, k ); - pFanout = Vec_PtrEntry( vMapEdges, 0 ); - Edge = Abc_ObjIsComplement(pFanout); - pFanout = Abc_ObjRegular(pFanout); - // make sure this is the same fanin - if ( Edge ) - assert( pLeaf == Abc_ObjFanin1(pFanout) ); - else - assert( pLeaf == Abc_ObjFanin0(pFanout) ); - nLatches = Seq_NodeCountLats(pFanout, Edge); - assert( nLatches == nLatchAfter ); - assert( nLatches > 0 ); - - // for each implicit latch add the real latch - pFanin = pLeaf->pCopy; - pRing = Seq_NodeGetRing(pFanout, Edge); - for ( m = 0, pLat = Seq_LatPrev(pRing); m < nLatches; m++, pLat = Seq_LatPrev(pLat) ) - { - pLatch = Abc_NtkCreateLatch( pNtkMap ); - pLatch->pData = (void *)Seq_LatInit(pLat); - Abc_ObjAddFanin( pLatch, pFanin ); - pFanin = pLatch; - } - // finally connect to the latch - Abc_ObjAddFanin( pAnd->pCopy, pFanin ); - } + // get the BDD of the node + pObj->pCopy->pData = Seq_FpgaMappingConnectBdd_rec( pNtk, pObj->Id << 8, NULL, -1, pObj, vLeaves ); + Cudd_Ref( pObj->pCopy->pData ); + // complement the BDD of the cut if it came from the opposite polarity choice cut +// if ( Vec_StrEntry(p->vPhase, i) ) +// pObj->pCopy->pData = Cudd_Not( pObj->pCopy->pData ); } - Vec_VecFree( vTotalEdges ); // set the POs Abc_NtkForEachPo( pNtk, pObj, i ) { - pFanin = Abc_ObjFanin0(pObj)->pCopy; - nLatches = Seq_NodeCountLats(pObj, 0); - assert( nLatches == Seq_ObjFaninL0(pObj) ); - if ( nLatches > 0 ) - { - pRing = Seq_NodeGetRing(pObj, 0); - for ( m = 0, pLat = Seq_LatPrev(pRing); m < nLatches; m++, pLat = Seq_LatPrev(pLat) ) - { - pLatch = Abc_NtkCreateLatch( pNtkMap ); - pLatch->pData = (void *)Seq_LatInit(pLat); - Abc_ObjAddFanin( pLatch, pFanin ); - pFanin = pLatch; - } - } - pFanin = Abc_ObjNotCond(pFanin, Abc_ObjFaninC0(pObj)); - Abc_ObjAddFanin( pObj->pCopy, pFanin ); + if ( pRing = Seq_NodeGetRing(pObj,0) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin0(pObj)->pCopy; + pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); } // add the latches and their names @@ -368,10 +324,10 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk ) Vec_PtrPush( pNtkMap->vCis, pLatch ); Vec_PtrPush( pNtkMap->vCos, pLatch ); } - // fix the problem with complemented and duplicated CO edges Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 ); - + // make the network minimum base + Abc_NtkMinimumBase( pNtkMap ); if ( !Abc_NtkCheck( pNtkMap ) ) fprintf( stdout, "Seq_NtkSeqFpgaMapped(): Network check has failed.\n" ); return pNtkMap; @@ -440,6 +396,52 @@ int Seq_FpgaMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vL /**Function************************************************************* + Synopsis [Collects the edges pointing to the leaves of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves ) +{ + Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1; + unsigned SeqEdge0, SeqEdge1; + int Lag, i; + // get the object and the lag + pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 ); + Lag = SeqEdge & 255; + // if the node is the fanin of the cut, return + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + if ( SeqEdge == (unsigned)pLeaf ) + return pObj->pCopy; + // continue unfolding + assert( Abc_NodeIsAigAnd(pObj) ); + // get new sequential edges + assert( Lag + Seq_ObjFaninL0(pObj) < 255 ); + assert( Lag + Seq_ObjFaninL1(pObj) < 255 ); + SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj); + SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj); + // call for the children + pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew ); + // solve subproblems + pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves ); + pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves ); + // add the fanins to the node + Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) ); + Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) ); + Seq_NodeDupLats( pObjNew, pObj, 0 ); + Seq_NodeDupLats( pObjNew, pObj, 1 ); + // set the lag of the new node equal to the internal lag plus mapping/retiming lag + Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) ); +// Seq_NodeSetLag( pObjNew, (char)(Lag) ); + return pObjNew; +} + +/**Function************************************************************* + Synopsis [Derives the BDD of the selected cut.] Description [] @@ -478,8 +480,6 @@ DdNode * Seq_FpgaMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqE bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); Cudd_RecursiveDeref( dd, bFunc0 ); Cudd_RecursiveDeref( dd, bFunc1 ); - // complement the function if the node is created from the complimented cut - // ... // return the BDD Cudd_Deref( bFunc ); return bFunc; @@ -537,18 +537,33 @@ void Seq_FpgaMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * p SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves ) +void Seq_FpgaMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ) { - Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1; + Seq_Lat_t * pRing; + Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew; unsigned SeqEdge0, SeqEdge1; - int Lag, i; + int Lag, i, k; // get the object and the lag pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 ); Lag = SeqEdge & 255; - // if the node is the fanin of the cut, return + // if the node is the fanin of the cut, add the connection and return Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + { if ( SeqEdge == (unsigned)pLeaf ) - return pObj->pCopy; + { + assert( pPrev != NULL ); + if ( pRing = Seq_NodeGetRing(pPrev,Edge) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy; + // check if the root already has this fanin + Abc_ObjForEachFanin( pRoot, pFanin, k ) + if ( pFanin == pFaninNew ) + return; + Abc_ObjAddFanin( pRoot->pCopy, pFaninNew ); + return; + } + } // continue unfolding assert( Abc_NodeIsAigAnd(pObj) ); // get new sequential edges @@ -557,19 +572,69 @@ Abc_Obj_t * Seq_FpgaMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, uns SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj); SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj); // call for the children - pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew ); - // solve subproblems - pFaninNew0 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves ); - pFaninNew1 = Seq_FpgaMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves ); - // add the fanins to the node - Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) ); - Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) ); - Seq_NodeDupLats( pObjNew, pObj, 0 ); - Seq_NodeDupLats( pObjNew, pObj, 1 ); - // set the lag of the new node equal to the internal lag plus mapping/retiming lag - Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) ); -// Seq_NodeSetLag( pObjNew, (char)(Lag) ); - return pObjNew; + Seq_FpgaMappingConnect_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves ); + Seq_FpgaMappingConnect_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves ); +} + +/**Function************************************************************* + + Synopsis [Collects the edges pointing to the leaves of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Seq_FpgaMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ) +{ + Seq_Lat_t * pRing; + Abc_Obj_t * pObj, * pLeaf, * pFanin, * pFaninNew; + unsigned SeqEdge0, SeqEdge1; + DdManager * dd = pRoot->pCopy->pNtk->pManFunc; + DdNode * bFunc, * bFunc0, * bFunc1; + int Lag, i, k; + // get the object and the lag + pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 ); + Lag = SeqEdge & 255; + // if the node is the fanin of the cut, add the connection and return + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + { + if ( SeqEdge == (unsigned)pLeaf ) + { + assert( pPrev != NULL ); + if ( pRing = Seq_NodeGetRing(pPrev,Edge) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin(pPrev,Edge)->pCopy; + // check if the root already has this fanin + Abc_ObjForEachFanin( pRoot->pCopy, pFanin, k ) + if ( pFanin == pFaninNew ) + return Cudd_bddIthVar( dd, k ); + Abc_ObjAddFanin( pRoot->pCopy, pFaninNew ); + return Cudd_bddIthVar( dd, k ); + } + } + // continue unfolding + assert( Abc_NodeIsAigAnd(pObj) ); + // get new sequential edges + assert( Lag + Seq_ObjFaninL0(pObj) < 255 ); + assert( Lag + Seq_ObjFaninL1(pObj) < 255 ); + SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj); + SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj); + // call for the children + bFunc0 = Seq_FpgaMappingConnectBdd_rec( pNtk, SeqEdge0, pObj, 0, pRoot, vLeaves ); Cudd_Ref( bFunc0 ); + bFunc1 = Seq_FpgaMappingConnectBdd_rec( pNtk, SeqEdge1, pObj, 1, pRoot, vLeaves ); Cudd_Ref( bFunc1 ); + bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pObj) ); + bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pObj) ); + // get the BDD of the node + bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( dd, bFunc0 ); + Cudd_RecursiveDeref( dd, bFunc1 ); + // return the BDD + Cudd_Deref( bFunc ); + return bFunc; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/seq/seqFpgaIter.c b/src/base/seq/seqFpgaIter.c index fc521158..9d4002bc 100644 --- a/src/base/seq/seqFpgaIter.c +++ b/src/base/seq/seqFpgaIter.c @@ -30,6 +30,7 @@ static void Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * static Cut_Cut_t * Seq_FpgaMappingSelectCut( Abc_Obj_t * pAnd ); extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ); +extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -53,9 +54,6 @@ void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose ) Abc_Obj_t * pObj; int i, clk; - // get the LUT library - p->nVarsMax = Fpga_LutLibReadVarMax( Abc_FrameReadLibLut() ); - // set defaults for cut computation memset( pParams, 0, sizeof(Cut_Params_t) ); pParams->nVarsMax = p->nVarsMax; // the max cut size ("k" of the k-feasible cuts) @@ -68,13 +66,16 @@ void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose ) // compute the cuts clk = clock(); p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams ); +// pParams->fSeq = 0; +// p->pCutMan = Abc_NtkCuts( pNtk, pParams ); p->timeCuts = clock() - clk; + if ( fVerbose ) Cut_ManPrintStats( p->pCutMan ); // compute the delays clk = clock(); - Seq_NtkRetimeDelayLags( pNtk, fVerbose ); + Seq_AigRetimeDelayLags( pNtk, fVerbose ); p->timeDelay = clock() - clk; // collect the nodes and cuts used in the mapping @@ -129,8 +130,6 @@ void Seq_FpgaMappingCollectNode_rec( Abc_Obj_t * pAnd, Vec_Ptr_t * vMapping, Vec Vec_PtrPush( vMapping, pAnd ); for ( k = 0; k < (int)pCutBest->nLeaves; k++ ) Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pCutBest->pLeaves[k] ); - -//printf( "Adding %d.\n", pAnd->Id ); } /**Function************************************************************* @@ -237,6 +236,9 @@ int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ) } // get the arrival time of the best non-trivial cut pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj ); + // skip the choice nodes + if ( pList == NULL ) + return SEQ_UPDATE_NO; lValueNew = ABC_INFINITY; for ( pCut = pList->pNext; pCut; pCut = pCut->pNext ) { @@ -249,8 +251,8 @@ int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ) // if ( lValueNew == lValueOld ) if ( lValueNew <= lValueOld ) return SEQ_UPDATE_NO; -//printf( "%d ", lValueNew ); Seq_NodeSetLValue( pObj, lValueNew ); +//printf( "%d -> %d ", lValueOld, lValueNew ); return SEQ_UPDATE_YES; } diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h index a39a6d69..4503cef8 100644 --- a/src/base/seq/seqInt.h +++ b/src/base/seq/seqInt.h @@ -27,6 +27,10 @@ #include "abc.h" #include "cut.h" +#include "main.h" +#include "mio.h" +#include "mapper.h" +#include "fpga.h" #include "seq.h" //////////////////////////////////////////////////////////////////////// @@ -52,15 +56,23 @@ struct Abc_Seq_t_ Vec_Ptr_t * vInits; // the initial states for each edge in the AIG Extra_MmFixed_t * pMmInits; // memory manager for latch structures used to remember init states int fVerbose; // the verbose flag + float fEpsilon; // the accuracy for delay computation + int fStandCells; // the flag denoting standard cell mapping + int nMaxIters; // the max number of iterations // K-feasible cuts int nVarsMax; // the max cut size Cut_Man_t * pCutMan; // cut manager + Map_SuperLib_t * pSuperLib; // the current supergate library // sequential arrival time computation Vec_Int_t * vLValues; // the arrival times (L-Values of nodes) + Vec_Int_t * vLValuesN; // the arrival times (L-Values of nodes) Vec_Str_t * vLags; // the lags of the mapped nodes + Vec_Str_t * vLagsN; // the lags of the mapped nodes + Vec_Str_t * vUses; // the phase usage // representation of the mapping Vec_Ptr_t * vMapAnds; // nodes visible in the mapping Vec_Vec_t * vMapCuts; // best cuts for each node + Vec_Vec_t * vMapDelays; // the delay of each fanin // runtime stats int timeCuts; // runtime to compute the cuts int timeDelay; // runtime to compute the L-values @@ -75,6 +87,7 @@ struct Seq_Lat_t_ { Seq_Lat_t * pNext; // the next Lat in the ring Seq_Lat_t * pPrev; // the prev Lat in the ring + Abc_Obj_t * pLatch; // the real latch corresponding to Lat }; // representation of latch on the edge @@ -94,6 +107,19 @@ struct Seq_RetStep_t_ // 1 word unsigned nLatches : 8; // the number of latches to retime }; +// representation of one mapping match +typedef struct Seq_Match_t_ Seq_Match_t; +struct Seq_Match_t_ // 3 words +{ + Abc_Obj_t * pAnd; // the AND gate used in the mapping + Cut_Cut_t * pCut; // the cut used to map it + Map_Super_t * pSuper; // the supergate used to implement the cut + unsigned fCompl : 1; // the polarity of the AND gate + unsigned fCutInv : 1; // the polarity of the cut + unsigned PolUse : 2; // the polarity use of this node + unsigned uPhase : 28; // the phase assignment at the boundary +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -124,9 +150,15 @@ static inline int Seq_ObjFaninLMax( Abc_Obj_t * pObj ) // reading l-values and lags static inline Vec_Int_t * Seq_NodeLValues( Abc_Obj_t * pNode ) { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValues; } +static inline Vec_Int_t * Seq_NodeLValuesN( Abc_Obj_t * pNode ) { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLValuesN; } static inline int Seq_NodeGetLValue( Abc_Obj_t * pNode ) { return Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id ); } static inline void Seq_NodeSetLValue( Abc_Obj_t * pNode, int Value ) { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Value ); } +static inline float Seq_NodeGetLValueP( Abc_Obj_t * pNode ) { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValues(pNode), (pNode)->Id ) ); } +static inline float Seq_NodeGetLValueN( Abc_Obj_t * pNode ) { return Abc_Int2Float( Vec_IntEntry( Seq_NodeLValuesN(pNode), (pNode)->Id ) ); } +static inline void Seq_NodeSetLValueP( Abc_Obj_t * pNode, float Value ) { Vec_IntWriteEntry( Seq_NodeLValues(pNode), (pNode)->Id, Abc_Float2Int(Value) ); } +static inline void Seq_NodeSetLValueN( Abc_Obj_t * pNode, float Value ) { Vec_IntWriteEntry( Seq_NodeLValuesN(pNode), (pNode)->Id, Abc_Float2Int(Value) ); } static inline int Seq_NodeComputeLag( int LValue, int Fi ) { return (LValue + 1024*Fi)/Fi - 1024 - (int)(LValue % Fi == 0); } +static inline int Seq_NodeComputeLagFloat( float LValue, float Fi ) { return ((int)ceil(LValue/Fi)) - 1; } // reading the contents of the lat static inline Abc_InitType_t Seq_LatInit( Seq_Lat_t * pLat ) { return ((unsigned)pLat->pPrev) & 3; } @@ -141,14 +173,22 @@ static inline void Seq_LatSetPrev( Seq_Lat_t * pLat, Seq_Lat_t * pPrev // accessing retiming lags static inline Cut_Man_t * Seq_NodeCutMan( Abc_Obj_t * pNode ) { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->pCutMan; } static inline Vec_Str_t * Seq_NodeLags( Abc_Obj_t * pNode ) { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLags; } +static inline Vec_Str_t * Seq_NodeLagsN( Abc_Obj_t * pNode ) { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vLagsN; } static inline char Seq_NodeGetLag( Abc_Obj_t * pNode ) { return Vec_StrEntry( Seq_NodeLags(pNode), (pNode)->Id ); } +static inline char Seq_NodeGetLagN( Abc_Obj_t * pNode ) { return Vec_StrEntry( Seq_NodeLagsN(pNode), (pNode)->Id ); } static inline void Seq_NodeSetLag( Abc_Obj_t * pNode, char Value ) { Vec_StrWriteEntry( Seq_NodeLags(pNode), (pNode)->Id, (Value) ); } +static inline void Seq_NodeSetLagN( Abc_Obj_t * pNode, char Value ) { Vec_StrWriteEntry( Seq_NodeLagsN(pNode), (pNode)->Id, (Value) ); } + +// phase usage +static inline Vec_Str_t * Seq_NodeUses( Abc_Obj_t * pNode ) { return ((Abc_Seq_t *)(pNode)->pNtk->pManFunc)->vUses; } +static inline char Seq_NodeGetUses( Abc_Obj_t * pNode ) { return Vec_StrEntry( Seq_NodeUses(pNode), (pNode)->Id ); } +static inline void Seq_NodeSetUses( Abc_Obj_t * pNode, char Value ) { Vec_StrWriteEntry( Seq_NodeUses(pNode), (pNode)->Id, (Value) ); } // accessing initial states static inline Vec_Ptr_t * Seq_NodeLats( Abc_Obj_t * pObj ) { return ((Abc_Seq_t*)pObj->pNtk->pManFunc)->vInits; } static inline Seq_Lat_t * Seq_NodeGetRing( Abc_Obj_t * pObj, int Edge ) { return Vec_PtrEntry( Seq_NodeLats(pObj), (pObj->Id<<1)+Edge ); } static inline void Seq_NodeSetRing( Abc_Obj_t * pObj, int Edge, Seq_Lat_t * pLat ) { Vec_PtrWriteEntry( Seq_NodeLats(pObj), (pObj->Id<<1)+Edge, pLat ); } -static inline Seq_Lat_t * Seq_NodeCreateLat( Abc_Obj_t * pObj ) { return (Seq_Lat_t *)Extra_MmFixedEntryFetch( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits ); } +static inline Seq_Lat_t * Seq_NodeCreateLat( Abc_Obj_t * pObj ) { Seq_Lat_t * p = (Seq_Lat_t *)Extra_MmFixedEntryFetch( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits ); p->pNext = p->pPrev = NULL; p->pLatch = NULL; return p; } static inline void Seq_NodeRecycleLat( Abc_Obj_t * pObj, Seq_Lat_t * pLat ) { Extra_MmFixedEntryRecycle( ((Abc_Seq_t*)pObj->pNtk->pManFunc)->pMmInits, (char *)pLat ); } // getting hold of the structure storing initial states of the latches @@ -167,18 +207,23 @@ static inline void Seq_NodeSetInitOne( Abc_Obj_t * pObj, int Edge, int /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== seqAigIter.c =============================================================*/ +extern void Seq_AigRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ); +extern int Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose ); +/*=== seqFpgaIter.c ============================================================*/ +extern void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose ); +extern int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ); +/*=== seqMapIter.c ============================================================*/ +extern void Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ); +/*=== seqRetIter.c =============================================================*/ +extern void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose ); /*=== seqLatch.c ===============================================================*/ extern void Seq_NodeInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init ); extern void Seq_NodeInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init ); extern Abc_InitType_t Seq_NodeDeleteFirst( Abc_Obj_t * pObj, int Edge ); extern Abc_InitType_t Seq_NodeDeleteLast( Abc_Obj_t * pObj, int Edge ); -/*=== seqFpgaIter.c ============================================================*/ -extern void Seq_FpgaMappingDelays( Abc_Ntk_t * pNtk, int fVerbose ); -extern int Seq_FpgaNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ); -/*=== seqRetIter.c =============================================================*/ -extern void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ); -extern int Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose ); /*=== seqUtil.c ================================================================*/ +extern int Seq_NtkLevelMax( Abc_Ntk_t * pNtk ); extern int Seq_ObjFanoutLMax( Abc_Obj_t * pObj ); extern int Seq_ObjFanoutLMin( Abc_Obj_t * pObj ); extern int Seq_ObjFanoutLSum( Abc_Obj_t * pObj ); diff --git a/src/base/seq/seqMan.c b/src/base/seq/seqMan.c index 109199fe..7dae5b23 100644 --- a/src/base/seq/seqMan.c +++ b/src/base/seq/seqMan.c @@ -49,12 +49,17 @@ Abc_Seq_t * Seq_Create( Abc_Ntk_t * pNtk ) memset( p, 0, sizeof(Abc_Seq_t) ); p->pNtk = pNtk; p->nSize = 1000; - p->pMmInits = Extra_MmFixedStart( sizeof(Seq_Lat_t) ); + p->nMaxIters = 15; + p->pMmInits = Extra_MmFixedStart( sizeof(Seq_Lat_t) ); + p->fEpsilon = (float)0.001; // create internal data structures - p->vNums = Vec_IntStart( 2 * p->nSize ); - p->vInits = Vec_PtrStart( 2 * p->nSize ); - p->vLValues = Vec_IntStart( p->nSize ); - p->vLags = Vec_StrStart( p->nSize ); + p->vNums = Vec_IntStart( 2 * p->nSize ); + p->vInits = Vec_PtrStart( 2 * p->nSize ); + p->vLValues = Vec_IntStart( p->nSize ); + p->vLags = Vec_StrStart( p->nSize ); + p->vLValuesN = Vec_IntStart( p->nSize ); + p->vLagsN = Vec_StrStart( p->nSize ); + p->vUses = Vec_StrStart( p->nSize ); return p; } @@ -78,6 +83,9 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId ) Vec_PtrFill( p->vInits, 2 * p->nSize, NULL ); Vec_IntFill( p->vLValues, p->nSize, 0 ); Vec_StrFill( p->vLags, p->nSize, 0 ); + Vec_IntFill( p->vLValuesN, p->nSize, 0 ); + Vec_StrFill( p->vLagsN, p->nSize, 0 ); + Vec_StrFill( p->vUses, p->nSize, 0 ); } @@ -94,10 +102,19 @@ void Seq_Resize( Abc_Seq_t * p, int nMaxId ) ***********************************************************************/ void Seq_Delete( Abc_Seq_t * p ) { + if ( p->fStandCells ) + { + void * pVoid; int i; + Vec_PtrForEachEntry( p->vMapAnds, pVoid, i ) + free( pVoid ); + } if ( p->vMapAnds ) Vec_PtrFree( p->vMapAnds ); // the nodes used in the mapping if ( p->vMapCuts ) Vec_VecFree( p->vMapCuts ); // the cuts used in the mapping if ( p->vLValues ) Vec_IntFree( p->vLValues ); // the arrival times (L-Values of nodes) if ( p->vLags ) Vec_StrFree( p->vLags ); // the lags of the mapped nodes + if ( p->vLValuesN ) Vec_IntFree( p->vLValuesN ); // the arrival times (L-Values of nodes) + if ( p->vLagsN ) Vec_StrFree( p->vLagsN ); // the lags of the mapped nodes + if ( p->vUses ) Vec_StrFree( p->vUses ); // the uses of phases if ( p->vInits ) Vec_PtrFree( p->vInits ); // the initial values of the latches if ( p->vNums ) Vec_IntFree( p->vNums ); // the numbers of latches Extra_MmFixedStop( p->pMmInits, 0 ); diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c index 8c72538b..4f5a5e73 100644 --- a/src/base/seq/seqMapCore.c +++ b/src/base/seq/seqMapCore.c @@ -19,18 +19,250 @@ ***********************************************************************/ #include "seqInt.h" +#include "main.h" +#include "mio.h" +#include "mapper.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk ); +extern int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose ); +extern Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk ); + +static int Seq_MapMappingCount( Abc_Ntk_t * pNtk ); +static int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves ); +static Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves ); +static DdNode * Seq_MapMappingBdd_rec( DdManager * dd, Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves ); +static void Seq_MapMappingEdges_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, Vec_Ptr_t * vLeaves, Vec_Vec_t * vMapEdges ); +static void Seq_MapMappingConnect_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); +static DdNode * Seq_MapMappingConnectBdd_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Abc_Obj_t * pPrev, int Edge, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); + + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Performs Map mapping and retiming.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Seq_MapRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Abc_Ntk_t * pNtkNew; + Abc_Ntk_t * pNtkMap; + int RetValue; + + // derive the supergate library + if ( Abc_FrameReadLibSuper() == NULL && Abc_FrameReadLibGen() ) + { + printf( "A simple supergate library is derived from gate library \"%s\".\n", + Mio_LibraryReadName(Abc_FrameReadLibGen()) ); + Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen() ); + } + p->pSuperLib = Abc_FrameReadLibSuper(); + p->nVarsMax = Map_SuperLibReadVarsMax(p->pSuperLib); + p->nMaxIters = nMaxIters; + p->fStandCells = 1; + + // find the best mapping and retiming for all nodes (p->vLValues, p->vBestCuts, p->vLags) + Seq_MapRetimeDelayLags( pNtk, fVerbose ); + if ( RetValue = Abc_NtkGetChoiceNum(pNtk) ) + { + printf( "The network has %d choices. Deriving the resulting network is skipped.\n", RetValue ); + return NULL; + } + return NULL; + + // duplicate the nodes contained in multiple cuts + pNtkNew = Seq_NtkMapDup( pNtk ); +// return pNtkNew; + + // implement the retiming + RetValue = Seq_NtkImplementRetiming( pNtkNew, ((Abc_Seq_t *)pNtkNew->pManFunc)->vLags, fVerbose ); + if ( RetValue == 0 ) + printf( "Retiming completed but initial state computation has failed.\n" ); +// return pNtkNew; + + // check the compatibility of initial states computed + if ( RetValue = Seq_NtkMapInitCompatible( pNtkNew, fVerbose ) ) + { + printf( "The number of LUTs with incompatible edges = %d.\n", RetValue ); + Abc_NtkDelete( pNtkNew ); + return NULL; + } + + // create the final mapped network + pNtkMap = Seq_NtkSeqMapMapped( pNtkNew ); + Abc_NtkDelete( pNtkNew ); + return pNtkMap; +} + +/**Function************************************************************* + + Synopsis [Derives the network by duplicating some of the nodes.] + + Description [Information about mapping is given as mapping nodes (p->vMapAnds) + and best cuts for each node (p->vMapCuts).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Seq_NtkMapDup( Abc_Ntk_t * pNtk ) +{ + Abc_Seq_t * pNew, * p = pNtk->pManFunc; + Seq_Match_t * pMatch; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pLeaf, * pDriver, * pDriverNew; + Vec_Ptr_t * vLeaves; + unsigned SeqEdge; + int i, k, nObjsNew, Lag; + + assert( Abc_NtkIsSeq(pNtk) ); + + // start the expanded network + pNtkNew = Abc_NtkStartFrom( pNtk, pNtk->ntkType, pNtk->ntkFunc ); + Abc_NtkCleanNext( pNtk ); + + // start the new sequential AIG manager + nObjsNew = 1 + Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Seq_MapMappingCount(pNtk); + Seq_Resize( pNtkNew->pManFunc, nObjsNew ); + + // duplicate the nodes in the mapping + Vec_PtrForEachEntry( p->vMapAnds, pMatch, i ) + if ( pMatch->fCompl ) + pMatch->pAnd->pNext = Abc_NtkCreateNode( pNtkNew ); + else + pMatch->pAnd->pCopy = Abc_NtkCreateNode( pNtkNew ); + + // recursively construct the internals of each node + Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) + { + vLeaves = Vec_VecEntry( p->vMapCuts, i ); + Seq_MapMappingBuild_rec( pNtkNew, pNtk, pObj->Id << 8, 1, Seq_NodeGetLag(pObj), vLeaves ); + } + assert( nObjsNew == pNtkNew->nObjs ); + + // set the POs + Abc_NtkForEachCo( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + pDriverNew = Abc_ObjFaninC0(pObj)? pDriver->pNext : pDriver->pCopy; + Abc_ObjAddFanin( pObj->pCopy, pDriverNew ); + } + + // duplicate the latches on the PO edges + Abc_NtkForEachPo( pNtk, pObj, i ) + Seq_NodeDupLats( pObj->pCopy, pObj, 0 ); + + // transfer the mapping info to the new manager + Vec_PtrForEachEntry( p->vMapAnds, pMatch, i ) + { + // convert the root node +// Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy ); + pMatch->pAnd = pMatch->pAnd->pCopy; + // get the leaves of the cut + vLeaves = Vec_VecEntry( p->vMapCuts, i ); + // convert the leaf nodes + Vec_PtrForEachEntry( vLeaves, pLeaf, k ) + { + SeqEdge = (unsigned)pLeaf; + pLeaf = Abc_NtkObj( pNtk, SeqEdge >> 8 ); +// Lag = (SeqEdge & 255);// + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf); + Lag = (SeqEdge & 255) + Seq_NodeGetLag(pObj) - Seq_NodeGetLag(pLeaf); + assert( Lag >= 0 ); + // translate the old leaf into the leaf in the new network + Vec_PtrWriteEntry( vLeaves, k, (void *)((pLeaf->pCopy->Id << 8) | Lag) ); +// printf( "%d -> %d\n", pLeaf->Id, pLeaf->pCopy->Id ); + } + } + pNew = pNtkNew->pManFunc; + pNew->nVarsMax = p->nVarsMax; + pNew->vMapAnds = p->vMapAnds; p->vMapAnds = NULL; + pNew->vMapCuts = p->vMapCuts; p->vMapCuts = NULL; + + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Seq_NtkMapDup(): Network check has failed.\n" ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Checks if the initial states are compatible.] + + Description [Checks of all the initial states on the fanins edges + of the cut have compatible number of latches and initial states. + If this is not true, then the mapped network with the does not have initial + state. Returns the number of LUTs with incompatible edges.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_NtkMapInitCompatible( Abc_Ntk_t * pNtk, int fVerbose ) +{ + return 1; +} + +/**Function************************************************************* + + Synopsis [Derives the final mapped network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk ) +{ + return NULL; +} + + + +/**Function************************************************************* + + Synopsis [Counts the number of nodes in the bag.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_MapMappingCount( Abc_Ntk_t * pNtk ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Vec_Ptr_t * vLeaves; + Abc_Obj_t * pAnd; + int i, Counter = 0; + Vec_PtrForEachEntry( p->vMapAnds, pAnd, i ) + { + vLeaves = Vec_VecEntry( p->vMapCuts, i ); + Counter += Seq_MapMappingCount_rec( pNtk, pAnd->Id << 8, vLeaves ); + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counts the number of nodes in the bag.] Description [] @@ -39,6 +271,76 @@ SeeAlso [] ***********************************************************************/ +int Seq_MapMappingCount_rec( Abc_Ntk_t * pNtk, unsigned SeqEdge, Vec_Ptr_t * vLeaves ) +{ + Abc_Obj_t * pObj, * pLeaf; + unsigned SeqEdge0, SeqEdge1; + int Lag, i; + // get the object and the lag + pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 ); + Lag = SeqEdge & 255; + // if the node is the fanin of the cut, return + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + if ( SeqEdge == (unsigned)pLeaf ) + return 0; + // continue unfolding + assert( Abc_NodeIsAigAnd(pObj) ); + // get new sequential edges + assert( Lag + Seq_ObjFaninL0(pObj) < 255 ); + assert( Lag + Seq_ObjFaninL1(pObj) < 255 ); + SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj); + SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj); + // call for the children + return 1 + Seq_MapMappingCount_rec( pNtk, SeqEdge0, vLeaves ) + + Seq_MapMappingCount_rec( pNtk, SeqEdge1, vLeaves ); +} + +/**Function************************************************************* + + Synopsis [Collects the edges pointing to the leaves of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Seq_MapMappingBuild_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, unsigned SeqEdge, int fTop, int LagCut, Vec_Ptr_t * vLeaves ) +{ + Abc_Obj_t * pObj, * pObjNew, * pLeaf, * pFaninNew0, * pFaninNew1; + unsigned SeqEdge0, SeqEdge1; + int Lag, i; + // get the object and the lag + pObj = Abc_NtkObj( pNtk, SeqEdge >> 8 ); + Lag = SeqEdge & 255; + // if the node is the fanin of the cut, return + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + if ( SeqEdge == (unsigned)pLeaf ) + return pObj->pCopy; + // continue unfolding + assert( Abc_NodeIsAigAnd(pObj) ); + // get new sequential edges + assert( Lag + Seq_ObjFaninL0(pObj) < 255 ); + assert( Lag + Seq_ObjFaninL1(pObj) < 255 ); + SeqEdge0 = (Abc_ObjFanin0(pObj)->Id << 8) + Lag + Seq_ObjFaninL0(pObj); + SeqEdge1 = (Abc_ObjFanin1(pObj)->Id << 8) + Lag + Seq_ObjFaninL1(pObj); + // call for the children + pObjNew = fTop? pObj->pCopy : Abc_NtkCreateNode( pNtkNew ); + // solve subproblems + pFaninNew0 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge0, 0, LagCut, vLeaves ); + pFaninNew1 = Seq_MapMappingBuild_rec( pNtkNew, pNtk, SeqEdge1, 0, LagCut, vLeaves ); + // add the fanins to the node + Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew0, Abc_ObjFaninC0(pObj) ) ); + Abc_ObjAddFanin( pObjNew, Abc_ObjNotCond( pFaninNew1, Abc_ObjFaninC1(pObj) ) ); + Seq_NodeDupLats( pObjNew, pObj, 0 ); + Seq_NodeDupLats( pObjNew, pObj, 1 ); + // set the lag of the new node equal to the internal lag plus mapping/retiming lag + Seq_NodeSetLag( pObjNew, (char)(Lag + LagCut) ); +// Seq_NodeSetLag( pObjNew, (char)(Lag) ); + return pObjNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/seq/seqMapIter.c b/src/base/seq/seqMapIter.c index 5f59ca50..5a8b57bd 100644 --- a/src/base/seq/seqMapIter.c +++ b/src/base/seq/seqMapIter.c @@ -19,10 +19,19 @@ ***********************************************************************/ #include "seqInt.h" +#include "main.h" +#include "mio.h" +#include "mapperInt.h" -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// +// the internal procedures +static float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose ); +static float Seq_MapRetimeSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose ); +static int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose ); +static int Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv ); +static float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts ); +static void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk ); + +extern Cut_Man_t * Abc_NtkSeqCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -30,7 +39,236 @@ /**Function************************************************************* - Synopsis [] + Synopsis [Computes the retiming lags for FPGA mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_MapRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Cut_Params_t Params, * pParams = &Params; + Abc_Obj_t * pObj; + float TotalArea, FiBest; + int i, clk; + + // set defaults for cut computation + memset( pParams, 0, sizeof(Cut_Params_t) ); + pParams->nVarsMax = p->nVarsMax; // the max cut size ("k" of the k-feasible cuts) + pParams->nKeepMax = 1000; // the max number of cuts kept at a node + pParams->fTruth = 1; // compute truth tables + pParams->fFilter = 1; // filter dominated cuts + pParams->fSeq = 1; // compute sequential cuts + pParams->fVerbose = fVerbose; // the verbosiness flag + + // compute the cuts +clk = clock(); + p->pCutMan = Abc_NtkSeqCuts( pNtk, pParams ); +p->timeCuts = clock() - clk; + if ( fVerbose ) + Cut_ManPrintStats( p->pCutMan ); + + // compute canonical forms of the truth tables of the cuts + Seq_MapCanonicizeTruthTables( pNtk ); + + // compute the delays +clk = clock(); + FiBest = Seq_MapRetimeDelayLagsInternal( pNtk, fVerbose ); +p->timeDelay = clock() - clk; + + // collect the nodes and cuts used in the mapping + p->vMapAnds = Vec_PtrAlloc( 1000 ); + p->vMapCuts = Vec_VecAlloc( 1000 ); + TotalArea = 0.0; + Abc_NtkForEachPo( pNtk, pObj, i ) + TotalArea += Seq_MapCollectNode_rec( Abc_ObjChild0(pObj), FiBest, p->vMapAnds, p->vMapCuts ); + + // clean the marks + Abc_NtkForEachObj( pNtk, pObj, i ) + pObj->fMarkA = pObj->fMarkB = 0; + + if ( fVerbose ) + printf( "Total area = %6.2f.\n", TotalArea ); + + // remove the cuts + Cut_ManStop( p->pCutMan ); + p->pCutMan = NULL; +} + +/**Function************************************************************* + + Synopsis [Retimes AIG for optimal delay using Pan's algorithm.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Seq_MapRetimeDelayLagsInternal( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Abc_Obj_t * pNode; + float FiMax, FiBest, Delta; + int i, RetValue; + char NodeLag; + + assert( Abc_NtkIsSeq( pNtk ) ); + + // assign the accuracy for min-period computation + Delta = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen()); + if ( Delta == 0.0 ) + { + Delta = Mio_LibraryReadDelayAnd2Max(Abc_FrameReadLibGen()); + if ( Delta == 0.0 ) + { + printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" ); + return 0.0; + } + } + + // get the upper bound on the clock period + FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk)); + Delta /= 2; + + // make sure this clock period is feasible + assert( Seq_MapRetimeForPeriod( pNtk, FiMax, fVerbose ) ); + + // search for the optimal clock period between 0 and nLevelMax + FiBest = Seq_MapRetimeSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose ); + + // recompute the best l-values + RetValue = Seq_MapRetimeForPeriod( pNtk, FiBest, fVerbose ); + assert( RetValue ); + + // write the retiming lags for both phases of each node + Vec_StrFill( p->vLags, p->nSize, 0 ); + Vec_StrFill( p->vLagsN, p->nSize, 0 ); + Abc_AigForEachAnd( pNtk, pNode, i ) + { + NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest ); + Seq_NodeSetLag( pNode, NodeLag ); + NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueN(pNode), FiBest ); + Seq_NodeSetLagN( pNode, NodeLag ); + } + + // print the result + if ( fVerbose ) + printf( "The best clock period is %6.2f.\n", FiBest ); + return FiBest; +} + +/**Function************************************************************* + + Synopsis [Performs binary search for the optimal clock period.] + + Description [Assumes that FiMin is infeasible while FiMax is feasible.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Seq_MapRetimeSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose ) +{ + float Median; + assert( FiMin < FiMax ); + if ( FiMin + Delta >= FiMax ) + return FiMax; + Median = FiMin + (FiMax - FiMin)/2; + if ( Seq_MapRetimeForPeriod( pNtk, Median, fVerbose ) ) + return Seq_MapRetimeSearch_rec( pNtk, FiMin, Median, Delta, fVerbose ); // Median is feasible + else + return Seq_MapRetimeSearch_rec( pNtk, Median, FiMax, Delta, fVerbose ); // Median is infeasible +} + +/**Function************************************************************* + + Synopsis [Returns 1 if retiming with this clock period is feasible.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_MapRetimeForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose ) +{ + Abc_Seq_t * p = pNtk->pManFunc; + Abc_Obj_t * pObj; + float DelayInv = Mio_LibraryReadDelayInvMax(Abc_FrameReadLibGen()); + int i, c, RetValue, fChange, Counter; + char * pReason = ""; + + // set l-values of all nodes to be minus infinity + Vec_IntFill( p->vLValues, p->nSize, -ABC_INFINITY ); + Vec_IntFill( p->vLValuesN, p->nSize, -ABC_INFINITY ); + Vec_StrFill( p->vUses, p->nSize, 0 ); + + // set l-values of constants and PIs + pObj = Abc_NtkObj( pNtk, 0 ); + Seq_NodeSetLValueP( pObj, 0.0 ); + Seq_NodeSetLValueN( pObj, 0.0 ); + Abc_NtkForEachPi( pNtk, pObj, i ) + { + Seq_NodeSetLValueP( pObj, 0.0 ); + Seq_NodeSetLValueN( pObj, DelayInv ); + } + + // update all values iteratively + Counter = 0; + for ( c = 0; c < p->nMaxIters; c++ ) + { + fChange = 0; + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Counter++; + RetValue = Seq_MapNodeUpdateLValue( pObj, Fi, DelayInv ); + if ( RetValue == SEQ_UPDATE_YES ) + fChange = 1; + } + Abc_NtkForEachPo( pNtk, pObj, i ) + { + RetValue = Seq_MapNodeUpdateLValue( pObj, Fi, DelayInv ); + if ( RetValue == SEQ_UPDATE_FAIL ) + break; + } + if ( RetValue == SEQ_UPDATE_FAIL ) + break; + if ( fChange == 0 ) + break; + } + if ( c == p->nMaxIters ) + { + RetValue = SEQ_UPDATE_FAIL; + pReason = "(timeout)"; + } + else + c++; + + // report the results + if ( fVerbose ) + { + if ( RetValue == SEQ_UPDATE_FAIL ) + printf( "Period = %6.2f. Iterations = %3d. Updates = %10d. Infeasible %s\n", Fi, c, Counter, pReason ); + else + printf( "Period = %6.2f. Iterations = %3d. Updates = %10d. Feasible\n", Fi, c, Counter ); + } + return RetValue != SEQ_UPDATE_FAIL; +} + + + + +/**Function************************************************************* + + Synopsis [Computes the l-value of the cut.] Description [] @@ -39,9 +277,280 @@ SeeAlso [] ***********************************************************************/ +float Seq_MapSuperGetArrival( Abc_Obj_t * pObj, float Fi, Seq_Match_t * pMatch, float DelayMax ) +{ + Abc_Seq_t * p = pObj->pNtk->pManFunc; + Abc_Obj_t * pFanin; + float lValueCur, lValueMax; + int i; + lValueMax = -ABC_INFINITY; + for ( i = pMatch->pCut->nLeaves - 1; i >= 0; i-- ) + { + // get the arrival time of the fanin + pFanin = Abc_NtkObj( pObj->pNtk, pMatch->pCut->pLeaves[i] >> 8 ); + if ( pMatch->uPhase & (1 << i) ) + lValueCur = Seq_NodeGetLValueN(pFanin) - Fi * (pMatch->pCut->pLeaves[i] & 255); + else + lValueCur = Seq_NodeGetLValueP(pFanin) - Fi * (pMatch->pCut->pLeaves[i] & 255); + // add the arrival time of this pin + if ( lValueMax < lValueCur + pMatch->pSuper->tDelaysR[i].Worst ) + lValueMax = lValueCur + pMatch->pSuper->tDelaysR[i].Worst; + if ( lValueMax < lValueCur + pMatch->pSuper->tDelaysF[i].Worst ) + lValueMax = lValueCur + pMatch->pSuper->tDelaysF[i].Worst; + if ( lValueMax > DelayMax + p->fEpsilon ) + return ABC_INFINITY; + } + return lValueMax; +} + +/**Function************************************************************* + + Synopsis [Computes the l-value of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Seq_MapNodeComputeCut( Abc_Obj_t * pObj, Cut_Cut_t * pCut, int fCompl, float Fi, Seq_Match_t * pMatchBest ) +{ + Seq_Match_t Match, * pMatchCur = &Match; + Abc_Seq_t * p = pObj->pNtk->pManFunc; + Map_Super_t * pSuper, * pSuperList; + unsigned uCanon[2]; + float lValueBest, lValueCur; + int i; + assert( pCut->nLeaves < 6 ); + // get the canonical truth table of this cut + uCanon[0] = uCanon[1] = (fCompl? pCut->uCanon0 : pCut->uCanon1); + // match the given phase of the cut + pSuperList = Map_SuperTableLookupC( p->pSuperLib, uCanon ); + // compute the arrival times of each supergate + lValueBest = ABC_INFINITY; + for ( pSuper = pSuperList; pSuper; pSuper = pSuper->pNext ) + { + // create the match + pMatchCur->pCut = pCut; + pMatchCur->pSuper = pSuper; + // get the phase + for ( i = 0; i < (int)pSuper->nPhases; i++ ) + { + pMatchCur->uPhase = (fCompl? pCut->Num0 : pCut->Num1) ^ pSuper->uPhases[i]; + // find the arrival time of this match + lValueCur = Seq_MapSuperGetArrival( pObj, Fi, pMatchCur, lValueBest ); + if ( lValueBest > lValueCur ) + { + lValueBest = lValueCur; + if ( pMatchBest ) + *pMatchBest = *pMatchCur; + } + } + } + return lValueBest; +} + +/**Function************************************************************* + + Synopsis [Computes the l-value of the node.] + + Description [The node can be internal or a PO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Seq_MapNodeComputePhase( Abc_Obj_t * pObj, int fCompl, float Fi, Seq_Match_t * pMatchBest ) +{ + Seq_Match_t Match, * pMatchCur = &Match; + Cut_Cut_t * pList, * pCut; + float lValueNew, lValueCut; + // get the list of cuts + pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj ); + // get the arrival time of the best non-trivial cut + lValueNew = ABC_INFINITY; + for ( pCut = pList->pNext; pCut; pCut = pCut->pNext ) + { + lValueCut = Seq_MapNodeComputeCut( pObj, pCut, fCompl, Fi, pMatchBest? pMatchCur : NULL ); + if ( lValueNew > lValueCut ) + { + lValueNew = lValueCut; + if ( pMatchBest ) + *pMatchBest = *pMatchCur; + } + } + return lValueNew; +} + +/**Function************************************************************* + + Synopsis [Computes the l-value of the node.] + + Description [The node can be internal or a PO.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_MapNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, float DelayInv ) +{ + Abc_Seq_t * p = pObj->pNtk->pManFunc; + Cut_Cut_t * pList; + char Use; + float lValueOld0, lValueOld1, lValue0, lValue1, lValue; + assert( !Abc_ObjIsPi(pObj) ); + assert( Abc_ObjFaninNum(pObj) > 0 ); + // consider the case of the PO + if ( Abc_ObjIsPo(pObj) ) + { + if ( Abc_ObjFaninC0(pObj) ) // PO requires negative polarity + lValue = Seq_NodeGetLValueN(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj); + else + lValue = Seq_NodeGetLValueP(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj); + return (lValue > Fi + p->fEpsilon)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO; + } + // get the cuts + pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj ); + if ( pList == NULL ) + return SEQ_UPDATE_NO; + // compute the arrival time of both phases + lValue0 = Seq_MapNodeComputePhase( pObj, 1, Fi, NULL ); + lValue1 = Seq_MapNodeComputePhase( pObj, 0, Fi, NULL ); + // consider the case when negative phase is too slow + if ( lValue0 > lValue1 + DelayInv + p->fEpsilon ) + lValue0 = lValue1 + DelayInv, Use = 2; + else if ( lValue1 > lValue0 + DelayInv + p->fEpsilon ) + lValue1 = lValue0 + DelayInv, Use = 1; + else + Use = 3; + // set the uses of the phases + Seq_NodeSetUses( pObj, Use ); + // get the old arrival times + lValueOld0 = Seq_NodeGetLValueN(pObj); + lValueOld1 = Seq_NodeGetLValueP(pObj); + // compare + if ( lValue0 <= lValueOld0 + p->fEpsilon && lValue1 <= lValueOld1 + p->fEpsilon ) + return SEQ_UPDATE_NO; + // update the values + if ( lValue0 > lValueOld0 + p->fEpsilon ) + Seq_NodeSetLValueN( pObj, lValue0 ); + if ( lValue1 > lValueOld1 + p->fEpsilon ) + Seq_NodeSetLValueP( pObj, lValue1 ); + return SEQ_UPDATE_YES; +} + + + +/**Function************************************************************* + + Synopsis [Derives the parameters of the best mapping/retiming for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +float Seq_MapCollectNode_rec( Abc_Obj_t * pAnd, float FiBest, Vec_Ptr_t * vMapping, Vec_Vec_t * vMapCuts ) +{ + Seq_Match_t * pMatch; + Abc_Obj_t * pFanin; + int k, fCompl, Use; + float Area; + + // get the polarity of the node + fCompl = Abc_ObjIsComplement(pAnd); + pAnd = Abc_ObjRegular(pAnd); + + // skip visited nodes + if ( fCompl ) + { + if ( pAnd->fMarkB ) + return 0.0; + pAnd->fMarkB = 1; + } + else + { + if ( pAnd->fMarkA ) + return 0.0; + pAnd->fMarkA = 1; + } + + // skip if this is a non-PI node + if ( !Abc_NodeIsAigAnd(pAnd) ) + { + if ( Abc_ObjIsPi(pAnd) && fCompl ) + return Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); + return 0.0; + } + + // check the uses of this node + Use = Seq_NodeGetUses( pAnd ); + if ( fCompl && Use == 2 ) // the neg phase is required; the pos phase is used + { + Area = Seq_MapCollectNode_rec( pAnd, FiBest, vMapping, vMapCuts ); + return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); + } + if ( !fCompl && Use == 1 ) // the pos phase is required; the neg phase is used + { + Area = Seq_MapCollectNode_rec( Abc_ObjNot(pAnd), FiBest, vMapping, vMapCuts ); + return Area + Mio_LibraryReadAreaInv(Abc_FrameReadLibGen()); + } + + // get the best match + pMatch = ALLOC( Seq_Match_t, 1 ); + Seq_MapNodeComputePhase( pAnd, fCompl, FiBest, pMatch ); + pMatch->pAnd = pAnd; + pMatch->fCompl = fCompl; + pMatch->fCutInv = pMatch->pCut->fCompl; + pMatch->PolUse = Use; + + // call for the fanin cuts + Area = pMatch->pSuper->Area; + for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ ) + { + pFanin = Abc_NtkObj( pAnd->pNtk, pMatch->pCut->pLeaves[k] >> 8 ); + if ( pMatch->uPhase & (1 << k) ) + pFanin = Abc_ObjNot( pFanin ); + Area += Seq_MapCollectNode_rec( pFanin, FiBest, vMapping, vMapCuts ); + } + + // add this node + Vec_PtrPush( vMapping, pMatch ); + for ( k = 0; k < (int)pMatch->pCut->nLeaves; k++ ) + Vec_VecPush( vMapCuts, Vec_PtrSize(vMapping)-1, (void *)pMatch->pCut->pLeaves[k] ); + + return Area; +} + +/**Function************************************************************* + + Synopsis [Computes the canonical versions of the truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_MapCanonicizeTruthTables( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + Cut_Cut_t * pCut, * pList; + int i; + Abc_AigForEachAnd( pNtk, pObj, i ) + { + pList = Abc_NodeReadCuts( Seq_NodeCutMan(pObj), pObj ); + for ( pCut = pList->pNext; pCut; pCut = pCut->pNext ) + Cut_TruthCanonicize( pCut ); + } +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c index 373e77bd..c746f9a4 100644 --- a/src/base/seq/seqRetCore.c +++ b/src/base/seq/seqRetCore.c @@ -6,7 +6,7 @@ PackageName [Construction and manipulation of sequential AIGs.] - Synopsis [The core of retiming procedures.] + Synopsis [The core of FPGA mapping/retiming package.] Author [Alan Mishchenko] @@ -19,36 +19,17 @@ ***********************************************************************/ #include "seqInt.h" +#include "dec.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/* - Retiming can be represented in three equivalent forms: - - as a set of integer lags for each node (array of chars by node ID) - - as a set of node numbers with lag for each, fwd and bwd (two arrays of Seq_RetStep_t_) - - as a set of latch moves over the nodes, fwd and bwd (two arrays of node pointers Abc_Obj_t *) -*/ - -static void Abc_ObjRetimeForward( Abc_Obj_t * pObj ); -static int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues ); -static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ); -static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ); - -static void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ); -static int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose ); -static void Abc_ObjRetimeForward( Abc_Obj_t * pObj ); -static int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues ); -static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ); -static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ); - -static Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward ); -static Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward ); -static Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward ); -static void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches ); -static void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches ); - +static Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk ); +static Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop ); +static void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init ); +static Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -56,7 +37,7 @@ static void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches ); /**Function************************************************************* - Synopsis [Performs performs optimal delay retiming.] + Synopsis [Performs FPGA mapping and retiming.] Description [] @@ -65,148 +46,31 @@ static void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches ); SeeAlso [] ***********************************************************************/ -void Seq_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ) +Abc_Ntk_t * Seq_NtkRetime( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbose ) { - Abc_Seq_t * p = pNtk->pManFunc; + Abc_Seq_t * p; + Abc_Ntk_t * pNtkAig, * pNtkNew; int RetValue; - if ( !fInitial ) - Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC ); - // get the retiming lags - Seq_NtkRetimeDelayLags( pNtk, fVerbose ); - // implement this retiming - RetValue = Seq_NtkImplementRetiming( pNtk, p->vLags, fVerbose ); + assert( !Abc_NtkHasAig(pNtk) ); + // derive the isomorphic seq AIG + pNtkAig = Seq_NtkRetimeDerive( pNtk ); + p = pNtkAig->pManFunc; + p->nMaxIters = nMaxIters; + // find the best mapping and retiming + Seq_NtkRetimeDelayLags( pNtk, pNtkAig, fVerbose ); + // implement the retiming + RetValue = Seq_NtkImplementRetiming( pNtkAig, p->vLags, fVerbose ); if ( RetValue == 0 ) printf( "Retiming completed but initial state computation has failed.\n" ); + // create the final mapped network + pNtkNew = Seq_NtkRetimeReconstruct( pNtk, pNtkAig ); + Abc_NtkDelete( pNtkAig ); + return pNtkNew; } /**Function************************************************************* - Synopsis [Performs most forward retiming.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Seq_NtkSeqRetimeForward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ) -{ - Vec_Ptr_t * vMoves; - Abc_Obj_t * pNode; - int i; - if ( !fInitial ) - Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC ); - // get the forward moves - vMoves = Abc_NtkUtilRetimingTry( pNtk, 1 ); - // undo the forward moves - Vec_PtrForEachEntryReverse( vMoves, pNode, i ) - Abc_ObjRetimeBackwardTry( pNode, 1 ); - // implement this forward retiming - Seq_NtkImplementRetimingForward( pNtk, vMoves ); - Vec_PtrFree( vMoves ); -} - -/**Function************************************************************* - - Synopsis [Performs most backward retiming.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Seq_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk, int fInitial, int fVerbose ) -{ - Vec_Ptr_t * vMoves; - Abc_Obj_t * pNode; - int i, RetValue; - if ( !fInitial ) - Seq_NtkLatchSetValues( pNtk, ABC_INIT_DC ); - // get the backward moves - vMoves = Abc_NtkUtilRetimingTry( pNtk, 0 ); - // undo the backward moves - Vec_PtrForEachEntryReverse( vMoves, pNode, i ) - Abc_ObjRetimeForwardTry( pNode, 1 ); - // implement this backward retiming - RetValue = Seq_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose ); - Vec_PtrFree( vMoves ); - if ( RetValue == 0 ) - printf( "Retiming completed but initial state computation has failed.\n" ); -} - - - - -/**Function************************************************************* - - Synopsis [Implements the retiming on the sequential AIG.] - - Description [Split the retiming into forward and backward.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Seq_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags, int fVerbose ) -{ - Vec_Int_t * vSteps; - Vec_Ptr_t * vMoves; - int RetValue; - - // forward retiming - vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 ); - // translate each set of steps into moves - if ( fVerbose ) - printf( "The number of forward steps = %6d.\n", Vec_IntSize(vSteps) ); - vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 ); - if ( fVerbose ) - printf( "The number of forward moves = %6d.\n", Vec_PtrSize(vMoves) ); - // implement this retiming - Seq_NtkImplementRetimingForward( pNtk, vMoves ); - Vec_IntFree( vSteps ); - Vec_PtrFree( vMoves ); - - // backward retiming - vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 ); - // translate each set of steps into moves - if ( fVerbose ) - printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) ); - vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 ); - if ( fVerbose ) - printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) ); - // implement this retiming - RetValue = Seq_NtkImplementRetimingBackward( pNtk, vMoves, fVerbose ); - Vec_IntFree( vSteps ); - Vec_PtrFree( vMoves ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Implements the given retiming on the sequential AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) -{ - Abc_Obj_t * pNode; - int i; - Vec_PtrForEachEntry( vMoves, pNode, i ) - Abc_ObjRetimeForward( pNode ); -} - -/**Function************************************************************* - - Synopsis [Retimes node forward by one latch.] + Synopsis [Derives the isomorphic seq AIG.] Description [] @@ -215,347 +79,118 @@ void Seq_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) SeeAlso [] ***********************************************************************/ -void Abc_ObjRetimeForward( Abc_Obj_t * pObj ) -{ - Abc_Obj_t * pFanout; - int Init0, Init1, Init, i; - assert( Abc_ObjFaninNum(pObj) == 2 ); - assert( Seq_ObjFaninL0(pObj) >= 1 ); - assert( Seq_ObjFaninL1(pObj) >= 1 ); - // remove the init values from the fanins - Init0 = Seq_NodeDeleteFirst( pObj, 0 ); - Init1 = Seq_NodeDeleteFirst( pObj, 1 ); - assert( Init0 != ABC_INIT_NONE ); - assert( Init1 != ABC_INIT_NONE ); - // take into account the complements in the node - if ( Abc_ObjFaninC0(pObj) ) - { - if ( Init0 == ABC_INIT_ZERO ) - Init0 = ABC_INIT_ONE; - else if ( Init0 == ABC_INIT_ONE ) - Init0 = ABC_INIT_ZERO; - } - if ( Abc_ObjFaninC1(pObj) ) - { - if ( Init1 == ABC_INIT_ZERO ) - Init1 = ABC_INIT_ONE; - else if ( Init1 == ABC_INIT_ONE ) - Init1 = ABC_INIT_ZERO; - } - // compute the value at the output of the node - if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO ) - Init = ABC_INIT_ZERO; - else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE ) - Init = ABC_INIT_ONE; - else - Init = ABC_INIT_DC; - - // make sure the label is clean - Abc_ObjForEachFanout( pObj, pFanout, i ) - assert( pFanout->fMarkC == 0 ); - // add the init values to the fanouts - Abc_ObjForEachFanout( pObj, pFanout, i ) - { - if ( pFanout->fMarkC ) - continue; - pFanout->fMarkC = 1; - if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) ) - Seq_NodeInsertLast( pFanout, Abc_ObjFanoutEdgeNum(pObj, pFanout), Init ); - else - { - assert( Abc_ObjFanin0(pFanout) == pObj ); - Seq_NodeInsertLast( pFanout, 0, Init ); - Seq_NodeInsertLast( pFanout, 1, Init ); - } - } - // clean the label - Abc_ObjForEachFanout( pObj, pFanout, i ) - pFanout->fMarkC = 0; -} - - -/**Function************************************************************* - - Synopsis [Implements the given retiming on the sequential AIG.] - - Description [Returns 0 of initial state computation fails.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int fVerbose ) +Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk ) { - Seq_RetEdge_t RetEdge; - stmm_table * tTable; - stmm_generator * gen; - Vec_Int_t * vValues; - Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf; - Abc_Obj_t * pNode, * pNodeNew; - int * pModel, RetValue, i, clk; - - // return if the retiming is trivial - if ( Vec_PtrSize(vMoves) == 0 ) - return 1; - - // create the network for the initial state computation - // start the table and the array of PO values - pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); - tTable = stmm_init_table( stmm_numcmp, stmm_numhash ); - vValues = Vec_IntAlloc( 100 ); - - // perform the backward moves and build the network for initial state computation - RetValue = 0; - Vec_PtrForEachEntry( vMoves, pNode, i ) - RetValue |= Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues ); - - // add the PIs corresponding to the white spots - stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew ) - Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) ); - - // add the PI/PO names - Abc_NtkAddDummyPiNames( pNtkProb ); - Abc_NtkAddDummyPoNames( pNtkProb ); - - // make sure everything is okay with the network structure - if ( !Abc_NtkDoCheck( pNtkProb ) ) + Abc_Seq_t * p; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin, * pFanout; + int i, k, RetValue; + char * pSop; + + // make sure it is an AIG without self-feeding latches + assert( !Abc_NtkHasAig(pNtk) ); + if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) ) + printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); + assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); + + if ( Abc_NtkIsBddLogic(pNtk) ) + Abc_NtkBddToSop(pNtk); + + // start the network + pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG ); + + // duplicate the name and the spec + pNtkNew->pName = util_strsav(pNtk->pName); + pNtkNew->pSpec = util_strsav(pNtk->pSpec); + // map the constant nodes + Abc_NtkCleanCopy( pNtk ); + // clone the PIs/POs/latches + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + + // create one AND for each logic node + Abc_NtkForEachNode( pNtk, pObj, i ) { - printf( "Seq_NtkImplementRetimingBackward: The internal network check has failed.\n" ); - Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); - Abc_NtkDelete( pNtkProb ); - stmm_free_table( tTable ); - Vec_IntFree( vValues ); - return 0; + pObj->pCopy = Abc_NtkCreateNode( pNtkNew ); + pObj->pCopy->pCopy = pObj; } + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy; - // check if conflict is found - if ( RetValue ) + // create internal AND nodes w/o strashing for each logic node (including constants) + Abc_NtkForEachNode( pNtk, pObj, i ) { - printf( "Seq_NtkImplementRetimingBackward: A top level conflict is detected. DC latch values are used.\n" ); - Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); - Abc_NtkDelete( pNtkProb ); - stmm_free_table( tTable ); - Vec_IntFree( vValues ); - return 0; - } - - // get the miter cone - pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues ); - Abc_NtkDelete( pNtkProb ); - Vec_IntFree( vValues ); - - if ( fVerbose ) - printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) ); - - // transform the miter into a logic network for efficient CNF construction - pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 ); - Abc_NtkDelete( pNtkMiter ); - - // solve the miter -clk = clock(); - RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 ); -if ( fVerbose ) -if ( clock() - clk > 100 ) -{ -PRT( "SAT solving time", clock() - clk ); -} - pModel = pNtkCnf->pModel; pNtkCnf->pModel = NULL; - Abc_NtkDelete( pNtkCnf ); - - // analyze the result - if ( RetValue == -1 || RetValue == 1 ) - { - Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); - if ( RetValue == 1 ) - printf( "Seq_NtkImplementRetimingBackward: The problem is unsatisfiable. DC latch values are used.\n" ); + // get the SOP of the node + if ( Abc_NtkHasMapping(pNtk) ) + pSop = Mio_GateReadSop(pObj->pData); else - printf( "Seq_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" ); - stmm_free_table( tTable ); - return 0; + pSop = pObj->pData; + pFanin = Seq_NodeRetimeDerive( pNtkNew, pObj, pSop ); + Abc_ObjAddFanin( pObj->pCopy, pFanin ); + Abc_ObjAddFanin( pObj->pCopy, pFanin ); } - // set the values of the latches - Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel ); - stmm_free_table( tTable ); - free( pModel ); - return 1; -} + // connect the POs... -/**Function************************************************************* + + // start the storage for initial states + p = pNtkNew->pManFunc; + Seq_Resize( p, Abc_NtkObjNumMax(pNtkNew) ); - Synopsis [Retimes node backward by one latch.] + // add the sequential edges + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjForEachFanout( pObj, pFanout, k ) + Seq_NodeAddEdges_rec( Abc_ObjFanin0(pObj)->pCopy, pFanout->pCopy, Abc_LatchInit(pObj) ); - Description [Constructs the problem for initial state computation. - Returns 1 if the conflict is found.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * tTable, Vec_Int_t * vValues ) -{ - Abc_Obj_t * pFanout; - Abc_InitType_t Init, Value; - Seq_RetEdge_t RetEdge; - Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuffer; - int i, Edge, fMet0, fMet1, fMetN; - - // make sure the node can be retimed - assert( Seq_ObjFanoutLMin(pObj) > 0 ); - // get the fanout values - fMet0 = fMet1 = fMetN = 0; - Abc_ObjForEachFanout( pObj, pFanout, i ) + // collect the nodes in the topological order + p->vMapAnds = Abc_NtkDfs( pNtk, 0 ); + p->vMapCuts = Vec_VecStart( Vec_PtrSize(p->vMapAnds) ); + p->vMapDelays = Vec_VecStart( Vec_PtrSize(p->vMapAnds) ); + Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) { - if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) + // change the node to be the new one + Vec_PtrWriteEntry( p->vMapAnds, i, pObj->pCopy ); + // collect the new fanins of this node + Abc_ObjForEachFanin( pObj, pFanin, k ) + Vec_VecPush( p->vMapCuts, i, pFanin->pCopy ); + // collect the delay info + if ( !Abc_NtkHasMapping(pNtk) ) { - Init = Seq_NodeGetInitLast( pFanout, 0 ); - if ( Init == ABC_INIT_ZERO ) - fMet0 = 1; - else if ( Init == ABC_INIT_ONE ) - fMet1 = 1; - else if ( Init == ABC_INIT_NONE ) - fMetN = 1; + Abc_ObjForEachFanin( pObj, pFanin, k ) + Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(1.0) ); } - if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) - { - Init = Seq_NodeGetInitLast( pFanout, 1 ); - if ( Init == ABC_INIT_ZERO ) - fMet0 = 1; - else if ( Init == ABC_INIT_ONE ) - fMet1 = 1; - else if ( Init == ABC_INIT_NONE ) - fMetN = 1; - } - } - - // consider the case when all fanout latches have don't-care values - // the new values on the fanin edges will be don't-cares - if ( !fMet0 && !fMet1 && !fMetN ) - { - // make sure the label is clean - Abc_ObjForEachFanout( pObj, pFanout, i ) - assert( pFanout->fMarkC == 0 ); - // update the fanout edges - Abc_ObjForEachFanout( pObj, pFanout, i ) - { - if ( pFanout->fMarkC ) - continue; - pFanout->fMarkC = 1; - if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) - Seq_NodeDeleteLast( pFanout, 0 ); - if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) - Seq_NodeDeleteLast( pFanout, 1 ); - } - // clean the label - Abc_ObjForEachFanout( pObj, pFanout, i ) - pFanout->fMarkC = 0; - // update the fanin edges - Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable ); - Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable ); - Seq_NodeInsertFirst( pObj, 0, ABC_INIT_DC ); - Seq_NodeInsertFirst( pObj, 1, ABC_INIT_DC ); - return 0; - } - // the initial values on the fanout edges contain 0, 1, or unknown - // the new values on the fanin edges will be unknown - - // add new AND-gate to the network - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); - - // add PO fanouts if any - if ( fMet0 ) - { - Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); - Vec_IntPush( vValues, 0 ); - } - if ( fMet1 ) - { - Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); - Vec_IntPush( vValues, 1 ); - } - - // make sure the label is clean - Abc_ObjForEachFanout( pObj, pFanout, i ) - assert( pFanout->fMarkC == 0 ); - // perform the changes - Abc_ObjForEachFanout( pObj, pFanout, i ) - { - if ( pFanout->fMarkC ) - continue; - pFanout->fMarkC = 1; - if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) - { - Edge = 0; - Value = Seq_NodeDeleteLast( pFanout, Edge ); - if ( Value != ABC_INIT_NONE ) - continue; - // value is unknown, remove it from the table - RetEdge.iNode = pFanout->Id; - RetEdge.iEdge = Edge; - RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed - if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) - assert( 0 ); - // create the fanout of the AND gate - Abc_ObjAddFanin( pFanoutNew, pNodeNew ); - } - if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) + else { - Edge = 1; - Value = Seq_NodeDeleteLast( pFanout, Edge ); - if ( Value != ABC_INIT_NONE ) - continue; - // value is unknown, remove it from the table - RetEdge.iNode = pFanout->Id; - RetEdge.iEdge = Edge; - RetEdge.iLatch = Seq_ObjFaninL( pFanout, Edge ); // after edge is removed - if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) - assert( 0 ); - // create the fanout of the AND gate - Abc_ObjAddFanin( pFanoutNew, pNodeNew ); + Mio_Pin_t * pPin = Mio_GateReadPins(pObj->pData); + float Max, tDelayBlockRise, tDelayBlockFall; + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin ); + tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin ); + Max = ABC_MAX( tDelayBlockRise, tDelayBlockFall ); + Vec_VecPush( p->vMapDelays, i, (void *)Abc_Float2Int(Max) ); + pPin = Mio_PinReadNext(pPin); + } } } - // clean the label - Abc_ObjForEachFanout( pObj, pFanout, i ) - pFanout->fMarkC = 0; - - // update the fanin edges - Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable ); - Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable ); - Seq_NodeInsertFirst( pObj, 0, ABC_INIT_NONE ); - Seq_NodeInsertFirst( pObj, 1, ABC_INIT_NONE ); - - // add the buffer - pBuffer = Abc_NtkCreateNode( pNtkNew ); - pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); - Abc_ObjAddFanin( pNodeNew, pBuffer ); - // point to it from the table - RetEdge.iNode = pObj->Id; - RetEdge.iEdge = 0; - RetEdge.iLatch = 0; - if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) ) - assert( 0 ); - // add the buffer - pBuffer = Abc_NtkCreateNode( pNtkNew ); - pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); - Abc_ObjAddFanin( pNodeNew, pBuffer ); - // point to it from the table - RetEdge.iNode = pObj->Id; - RetEdge.iEdge = 1; - RetEdge.iLatch = 0; - if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pBuffer ) ) - assert( 0 ); + // set the cutset composed of latch drivers +// Abc_NtkAigCutsetCopy( pNtk ); + Seq_NtkLatchGetEqualFaninNum( pNtkNew ); - // report conflict is found - return fMet0 && fMet1; + // copy EXDC and check correctness + if ( pNtkNew->pExdc ) + fprintf( stdout, "Warning: EXDC is not copied when converting to sequential AIG.\n" ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Seq_NtkRetimeDerive(): Network check has failed.\n" ); + return pNtkNew; } /**Function************************************************************* - Synopsis [Generates the printable edge label with the initial state.] + Synopsis [Add sequential edges.] Description [] @@ -564,37 +199,27 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t SeeAlso [] ***********************************************************************/ -void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ) +void Seq_NodeAddEdges_rec( Abc_Obj_t * pGoal, Abc_Obj_t * pNode, Abc_InitType_t Init ) { - Abc_Obj_t * pFanoutNew; - Seq_RetEdge_t RetEdge; - Abc_InitType_t Init; - int nLatches, i; - - // get the number of latches on the edge - nLatches = Seq_ObjFaninL( pObj, Edge ); - for ( i = nLatches - 1; i >= 0; i-- ) - { - // get the value of this latch - Init = Seq_NodeGetInitOne( pObj, Edge, i ); - if ( Init != ABC_INIT_NONE ) - continue; - // get the retiming edge - RetEdge.iNode = pObj->Id; - RetEdge.iEdge = Edge; - RetEdge.iLatch = i; - // remove entry from table and add it with a different key - if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) - assert( 0 ); - RetEdge.iLatch++; - if ( stmm_insert( tTable, (char *)Seq_RetEdge2Int(RetEdge), (char *)pFanoutNew ) ) - assert( 0 ); - } + Abc_Obj_t * pFanin; + // consider the first fanin + pFanin = Abc_ObjFanin0(pNode); + if ( pFanin->pCopy == NULL ) // internal node + Seq_NodeAddEdges_rec( pGoal, pFanin, Init ); + else if ( pFanin == pGoal ) + Seq_NodeInsertFirst( pNode, 0, Init ); + // consider the second fanin + pFanin = Abc_ObjFanin1(pNode); + if ( pFanin->pCopy == NULL ) // internal node + Seq_NodeAddEdges_rec( pGoal, pFanin, Init ); + else if ( pFanin == pGoal ) + Seq_NodeInsertFirst( pNode, 1, Init ); } + /**Function************************************************************* - Synopsis [Sets the initial values.] + Synopsis [Strashes one logic node using its SOP.] Description [] @@ -603,29 +228,45 @@ void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * t SeeAlso [] ***********************************************************************/ -void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ) +Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop ) { - Abc_Obj_t * pNode; - stmm_generator * gen; - Seq_RetEdge_t RetEdge; - Abc_InitType_t Init; - int i; - - i = 0; - stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL ) + Dec_Graph_t * pFForm; + Dec_Node_t * pNode; + Abc_Obj_t * pAnd; + int i, nFanins; + + // get the number of node's fanins + nFanins = Abc_ObjFaninNum( pRoot ); + assert( nFanins == Abc_SopGetVarNum(pSop) ); + if ( nFanins < 2 ) { - pNode = Abc_NtkObj( pNtk, RetEdge.iNode ); - Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC; - Seq_NodeSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init ); - i++; + if ( Abc_SopIsConst1(pSop) ) + return Abc_NtkConst1(pNtkNew); + else if ( Abc_SopIsConst0(pSop) ) + return Abc_ObjNot( Abc_NtkConst1(pNtkNew) ); + else if ( Abc_SopIsBuf(pSop) ) + return Abc_ObjFanin0(pRoot)->pCopy; + else if ( Abc_SopIsInv(pSop) ) + return Abc_ObjNot( Abc_ObjFanin0(pRoot)->pCopy ); + assert( 0 ); + return NULL; } -} + // perform factoring + pFForm = Dec_Factor( pSop ); + // collect the fanins + Dec_GraphForEachLeaf( pFForm, pNode, i ) + pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy; + // perform strashing + pAnd = Dec_GraphToNetworkNoStrash( pNtkNew, pFForm ); + Dec_GraphFree( pFForm ); + return pAnd; +} /**Function************************************************************* - Synopsis [Performs forward retiming of the sequential AIG.] + Synopsis [Reconstructs the network after retiming.] Description [] @@ -634,333 +275,66 @@ void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward ) +Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk ) { - Vec_Ptr_t * vNodes, * vMoves; - Abc_Obj_t * pNode, * pFanout, * pFanin; - int i, k, nLatches; - assert( Abc_NtkIsSeq( pNtk ) ); - // assume that all nodes can be retimed - vNodes = Vec_PtrAlloc( 100 ); - Abc_AigForEachAnd( pNtk, pNode, i ) - { - Vec_PtrPush( vNodes, pNode ); - pNode->fMarkA = 1; - } - // process the nodes - vMoves = Vec_PtrAlloc( 100 ); - Vec_PtrForEachEntry( vNodes, pNode, i ) - { -// printf( "(%d,%d) ", Seq_ObjFaninL0(pNode), Seq_ObjFaninL0(pNode) ); - // unmark the node as processed - pNode->fMarkA = 0; - // get the number of latches to retime - if ( fForward ) - nLatches = Seq_ObjFaninLMin(pNode); - else - nLatches = Seq_ObjFanoutLMin(pNode); - if ( nLatches == 0 ) - continue; - assert( nLatches > 0 ); - // retime the latches forward - if ( fForward ) - Abc_ObjRetimeForwardTry( pNode, nLatches ); - else - Abc_ObjRetimeBackwardTry( pNode, nLatches ); - // write the moves - for ( k = 0; k < nLatches; k++ ) - Vec_PtrPush( vMoves, pNode ); - // schedule fanouts for updating - if ( fForward ) - { - Abc_ObjForEachFanout( pNode, pFanout, k ) - { - if ( Abc_ObjFaninNum(pFanout) != 2 || pFanout->fMarkA ) - continue; - pFanout->fMarkA = 1; - Vec_PtrPush( vNodes, pFanout ); - } - } - else - { - Abc_ObjForEachFanin( pNode, pFanin, k ) - { - if ( Abc_ObjFaninNum(pFanin) != 2 || pFanin->fMarkA ) - continue; - pFanin->fMarkA = 1; - Vec_PtrPush( vNodes, pFanin ); - } - } - } - Vec_PtrFree( vNodes ); - // make sure the marks are clean the the retiming is final - Abc_AigForEachAnd( pNtk, pNode, i ) - { - assert( pNode->fMarkA == 0 ); - if ( fForward ) - assert( Seq_ObjFaninLMin(pNode) == 0 ); - else - assert( Seq_ObjFanoutLMin(pNode) == 0 ); - } - return vMoves; -} + Abc_Seq_t * p = pNtk->pManFunc; + Seq_Lat_t * pRing; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFaninNew, * pObjNew; + int i; -/**Function************************************************************* + assert( !Abc_NtkIsSeq(pNtkOld) ); + assert( Abc_NtkIsSeq(pNtk) ); - Synopsis [Translates retiming steps into retiming moves.] + // start the final network + pNtkNew = Abc_NtkStartFrom( pNtk, pNtkOld->ntkType, pNtkOld->ntkFunc ); - Description [] - - SideEffects [] + // copy the internal nodes + Abc_NtkForEachNode( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj ); - SeeAlso [] + // share the latches + Seq_NtkShareLatches( pNtkNew, pNtk ); -***********************************************************************/ -Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vSteps, bool fForward ) -{ - Seq_RetStep_t RetStep; - Vec_Ptr_t * vMoves; - Abc_Obj_t * pNode; - int i, k, iNode, nLatches, Number; - int fChange; - assert( Abc_NtkIsSeq( pNtk ) ); - -/* - // try implementing all the moves at once - Vec_IntForEachEntry( vSteps, Number, i ) + // connect the objects + Abc_AigForEachAnd( pNtk, pObj, i ) { - // get the retiming step - RetStep = Seq_Int2RetStep( Number ); - // get the node to be retimed - pNode = Abc_NtkObj( pNtk, RetStep.iNode ); - assert( RetStep.nLatches > 0 ); - nLatches = RetStep.nLatches; - - if ( fForward ) - Abc_ObjRetimeForwardTry( pNode, nLatches ); + if ( pRing = Seq_NodeGetRing(pObj,0) ) + pFaninNew = pRing->pLatch; else - Abc_ObjRetimeBackwardTry( pNode, nLatches ); - } - // now look if any node has wrong number of latches - Abc_AigForEachAnd( pNtk, pNode, i ) - { - if ( Seq_ObjFaninL0(pNode) < 0 ) - printf( "Wrong 0node %d.\n", pNode->Id ); - if ( Seq_ObjFaninL1(pNode) < 0 ) - printf( "Wrong 1node %d.\n", pNode->Id ); - } - // try implementing all the moves at once - Vec_IntForEachEntry( vSteps, Number, i ) - { - // get the retiming step - RetStep = Seq_Int2RetStep( Number ); - // get the node to be retimed - pNode = Abc_NtkObj( pNtk, RetStep.iNode ); - assert( RetStep.nLatches > 0 ); - nLatches = RetStep.nLatches; - - if ( !fForward ) - Abc_ObjRetimeForwardTry( pNode, nLatches ); - else - Abc_ObjRetimeBackwardTry( pNode, nLatches ); - } -*/ + pFaninNew = Abc_ObjFanin0(pObj)->pCopy; + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); - // process the nodes - vMoves = Vec_PtrAlloc( 100 ); - while ( Vec_IntSize(vSteps) > 0 ) - { - iNode = 0; - fChange = 0; - Vec_IntForEachEntry( vSteps, Number, i ) - { - // get the retiming step - RetStep = Seq_Int2RetStep( Number ); - // get the node to be retimed - pNode = Abc_NtkObj( pNtk, RetStep.iNode ); - assert( RetStep.nLatches > 0 ); - // get the number of latches that can be retimed - if ( fForward ) - nLatches = Seq_ObjFaninLMin(pNode); - else - nLatches = Seq_ObjFanoutLMin(pNode); - if ( nLatches == 0 ) - { - Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) ); - continue; - } - assert( nLatches > 0 ); - fChange = 1; - // get the number of latches to be retimed over this node - nLatches = ABC_MIN( nLatches, (int)RetStep.nLatches ); - // retime the latches forward - if ( fForward ) - Abc_ObjRetimeForwardTry( pNode, nLatches ); - else - Abc_ObjRetimeBackwardTry( pNode, nLatches ); - // write the moves - for ( k = 0; k < nLatches; k++ ) - Vec_PtrPush( vMoves, pNode ); - // subtract the retiming performed - RetStep.nLatches -= nLatches; - // store the node if it is not retimed completely - if ( RetStep.nLatches > 0 ) - Vec_IntWriteEntry( vSteps, iNode++, Seq_RetStep2Int(RetStep) ); - } - // reduce the array - Vec_IntShrink( vSteps, iNode ); - if ( !fChange ) - { - printf( "Warning: %d strange steps (a minor bug to be fixed later).\n", Vec_IntSize(vSteps) ); -/* - Vec_IntForEachEntry( vSteps, Number, i ) - { - RetStep = Seq_Int2RetStep( Number ); - printf( "%d(%d) ", RetStep.iNode, RetStep.nLatches ); - } - printf( "\n" ); -*/ - break; - } - } - // undo the tentative retiming - if ( fForward ) - { - Vec_PtrForEachEntryReverse( vMoves, pNode, i ) - Abc_ObjRetimeBackwardTry( pNode, 1 ); - } - else - { - Vec_PtrForEachEntryReverse( vMoves, pNode, i ) - Abc_ObjRetimeForwardTry( pNode, 1 ); - } - return vMoves; -} - - -/**Function************************************************************* - - Synopsis [Splits retiming into forward and backward.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward ) -{ - Vec_Int_t * vNodes; - Seq_RetStep_t RetStep; - int Value, i; - vNodes = Vec_IntAlloc( 100 ); - Vec_StrForEachEntry( vLags, Value, i ) - { - if ( Value < 0 && fForward ) - { - RetStep.iNode = i; - RetStep.nLatches = -Value; - Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) ); - } - else if ( Value > 0 && !fForward ) - { - RetStep.iNode = i; - RetStep.nLatches = Value; - Vec_IntPush( vNodes, Seq_RetStep2Int(RetStep) ); - } + if ( pRing = Seq_NodeGetRing(pObj,1) ) + pFaninNew = pRing->pLatch; + else + pFaninNew = Abc_ObjFanin1(pObj)->pCopy; + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); } - return vNodes; -} - -/**Function************************************************************* - - Synopsis [Retime node forward without initial states.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_ObjRetimeForwardTry( Abc_Obj_t * pObj, int nLatches ) -{ - Abc_Obj_t * pFanout; - int i; - // make sure it is an AND gate - assert( Abc_ObjFaninNum(pObj) == 2 ); - // make sure it has enough latches -// assert( Seq_ObjFaninL0(pObj) >= nLatches ); -// assert( Seq_ObjFaninL1(pObj) >= nLatches ); - // subtract these latches on the fanin side - Seq_ObjAddFaninL0( pObj, -nLatches ); - Seq_ObjAddFaninL1( pObj, -nLatches ); - // make sure the label is clean - Abc_ObjForEachFanout( pObj, pFanout, i ) - assert( pFanout->fMarkC == 0 ); - // add these latches on the fanout side - Abc_ObjForEachFanout( pObj, pFanout, i ) + // connect the POs + Abc_NtkForEachPo( pNtk, pObj, i ) { - if ( pFanout->fMarkC ) - continue; - pFanout->fMarkC = 1; - if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) ) - Seq_ObjAddFanoutL( pObj, pFanout, nLatches ); + if ( pRing = Seq_NodeGetRing(pObj,0) ) + pFaninNew = pRing->pLatch; else - { - assert( Abc_ObjFanin0(pFanout) == pObj ); - Seq_ObjAddFaninL0( pFanout, nLatches ); - Seq_ObjAddFaninL1( pFanout, nLatches ); - } + pFaninNew = Abc_ObjFanin0(pObj)->pCopy; + pFaninNew = Abc_ObjNotCond( pFaninNew, Abc_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); } - // clean the label - Abc_ObjForEachFanout( pObj, pFanout, i ) - pFanout->fMarkC = 0; -} - -/**Function************************************************************* - Synopsis [Retime node backward without initial states.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_ObjRetimeBackwardTry( Abc_Obj_t * pObj, int nLatches ) -{ - Abc_Obj_t * pFanout; - int i; - // make sure it is an AND gate - assert( Abc_ObjFaninNum(pObj) == 2 ); - // make sure the label is clean - Abc_ObjForEachFanout( pObj, pFanout, i ) - assert( pFanout->fMarkC == 0 ); - // subtract these latches on the fanout side - Abc_ObjForEachFanout( pObj, pFanout, i ) + // add the latches and their names + Abc_NtkAddDummyLatchNames( pNtkNew ); + Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) { - if ( pFanout->fMarkC ) - continue; - pFanout->fMarkC = 1; -// assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches ); - if ( Abc_ObjFaninId0(pFanout) != Abc_ObjFaninId1(pFanout) ) - Seq_ObjAddFanoutL( pObj, pFanout, -nLatches ); - else - { - assert( Abc_ObjFanin0(pFanout) == pObj ); - Seq_ObjAddFaninL0( pFanout, -nLatches ); - Seq_ObjAddFaninL1( pFanout, -nLatches ); - } + Vec_PtrPush( pNtkNew->vCis, pObjNew ); + Vec_PtrPush( pNtkNew->vCos, pObjNew ); } - // clean the label - Abc_ObjForEachFanout( pObj, pFanout, i ) - pFanout->fMarkC = 0; - // add these latches on the fanin side - Seq_ObjAddFaninL0( pObj, nLatches ); - Seq_ObjAddFaninL1( pObj, nLatches ); + // fix the problem with complemented and duplicated CO edges + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkSeqToLogicSop(): Network check has failed.\n" ); + return pNtkNew; + } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/seq/seqRetIter.c b/src/base/seq/seqRetIter.c index 6f7a320a..5c65e72e 100644 --- a/src/base/seq/seqRetIter.c +++ b/src/base/seq/seqRetIter.c @@ -6,7 +6,7 @@ PackageName [Construction and manipulation of sequential AIGs.] - Synopsis [The iterative L-Value computation for retiming procedures.] + Synopsis [Iterative delay computation in FPGA mapping/retiming package.] Author [Alan Mishchenko] @@ -19,15 +19,17 @@ ***********************************************************************/ #include "seqInt.h" +#include "main.h" +#include "fpga.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -// the internal procedures -static int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose ); -static int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose ); -static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ); +static float Seq_NtkMappingSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose ); +static int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose ); +static int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays ); +static void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -35,7 +37,7 @@ static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ); /**Function************************************************************* - Synopsis [Retimes AIG for optimal delay using Pan's algorithm.] + Synopsis [Computes the retiming lags for arbitrary network.] Description [] @@ -44,73 +46,67 @@ static int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ); SeeAlso [] ***********************************************************************/ -void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ) +void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtk, int fVerbose ) { Abc_Seq_t * p = pNtk->pManFunc; Abc_Obj_t * pNode; - int i, FiMax, FiBest, RetValue; + float FiMax, FiBest, Delta; + int i, RetValue; char NodeLag; assert( Abc_NtkIsSeq( pNtk ) ); - // get the upper bound on the clock period -// FiMax = Abc_NtkNodeNum(pNtk); - FiMax = 0; - Abc_AigForEachAnd( pNtk, pNode, i ) - if ( FiMax < (int)pNode->Level ) - FiMax = pNode->Level; - FiMax += 2; + // the root AND gates and node delay should be assigned + assert( p->vMapAnds ); + assert( p->vMapCuts ); + assert( p->vMapDelays ); + + // guess the upper bound on the clock period + if ( Abc_NtkHasMapping(pNtkOld) ) + { + // assign the accuracy for min-period computation + Delta = Mio_LibraryReadDelayNand2Max(Abc_FrameReadLibGen()); + if ( Delta == 0.0 ) + { + Delta = Mio_LibraryReadDelayAnd2Max(Abc_FrameReadLibGen()); + if ( Delta == 0.0 ) + { + printf( "Cannot retime/map if the library does not have NAND2 or AND2.\n" ); + return; + } + } + // get the upper bound on the clock period + FiMax = Delta * (2 + Seq_NtkLevelMax(pNtk)); + Delta /= 2; + } + else + { + FiMax = (float)2.0 + Abc_NtkGetLevelNum(pNtkOld); + Delta = 1; + } // make sure this clock period is feasible - assert( Seq_RetimeForPeriod( pNtk, FiMax, fVerbose ) ); + assert( Seq_NtkMappingForPeriod( pNtk, FiMax, fVerbose ) ); // search for the optimal clock period between 0 and nLevelMax - FiBest = Seq_RetimeSearch_rec( pNtk, 0, FiMax, fVerbose ); + FiBest = Seq_NtkMappingSearch_rec( pNtk, 0.0, FiMax, Delta, fVerbose ); // recompute the best l-values - RetValue = Seq_RetimeForPeriod( pNtk, FiBest, fVerbose ); + RetValue = Seq_NtkMappingForPeriod( pNtk, FiBest, fVerbose ); assert( RetValue ); - // write the retiming lags - Vec_StrFill( p->vLags, p->nSize, 0 ); - Abc_AigForEachAnd( pNtk, pNode, i ) - { - NodeLag = Seq_NodeComputeLag( Seq_NodeGetLValue(pNode), FiBest ); - Seq_NodeSetLag( pNode, NodeLag ); - } -/* + // write the retiming lags for both phases of each node + Vec_StrFill( p->vLags, p->nSize, 0 ); + Vec_PtrForEachEntry( p->vMapAnds, pNode, i ) { - Abc_Obj_t * pFanin, * pFanout; - pNode = Abc_NtkObj( pNtk, 823 ); - printf( "Node %d. Lag = %d. LValue = %d. Latches = (%d,%d) (%d,%d).\n", pNode->Id, Seq_NodeGetLag(pNode), Seq_NodeGetLValue(pNode), - Seq_ObjFaninL0(pNode), Seq_ObjFaninL1(pNode), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 826)), Seq_ObjFanoutL(pNode, Abc_NtkObj(pNtk, 1210)) ); - pFanin = Abc_ObjFanin0( pNode ); - printf( "Fanin %d. Lag = %d. LValue = %d. Latches = (%d,%d)\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin), - Seq_ObjFaninL0(pFanin), Seq_ObjFaninL1(pFanin) ); - pFanin = Abc_ObjFanin1( pNode ); - printf( "Fanin %d. Lag = %d. LValue = %d.\n", pFanin->Id, Seq_NodeGetLag(pFanin), Seq_NodeGetLValue(pFanin) ); - Abc_ObjForEachFanout( pNode, pFanout, i ) - printf( "Fanout %d. Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) ); - Abc_ObjForEachFanout( Abc_ObjFanin0(pNode), pFanout, i ) - printf( "Fanout %d. Lag = %d. LValue = %d.\n", pFanout->Id, Seq_NodeGetLag(pFanout), Seq_NodeGetLValue(pFanout) ); + NodeLag = Seq_NodeComputeLagFloat( Seq_NodeGetLValueP(pNode), FiBest ); +// Seq_NodeSetLag( pNode, NodeLag ); + Seq_NodeRetimeSetLag_rec( pNode, NodeLag ); } -*/ // print the result if ( fVerbose ) - printf( "The best clock period is %3d.\n", FiBest ); - -/* - printf( "LValues : " ); - Abc_AigForEachAnd( pNtk, pNode, i ) - printf( "%d=%d ", i, Seq_NodeGetLValue(pNode) ); - printf( "\n" ); - printf( "Lags : " ); - Abc_AigForEachAnd( pNtk, pNode, i ) - if ( Vec_StrEntry(p->vLags,i) != 0 ) - printf( "%d=%d(%d)(%d) ", i, Vec_StrEntry(p->vLags,i), Seq_NodeGetLValue(pNode), Seq_NodeGetLValue(pNode) - FiBest * Vec_StrEntry(p->vLags,i) ); - printf( "\n" ); -*/ + printf( "The best clock period is %6.2f.\n", FiBest ); } /**Function************************************************************* @@ -124,17 +120,17 @@ void Seq_NtkRetimeDelayLags( Abc_Ntk_t * pNtk, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose ) +float Seq_NtkMappingSearch_rec( Abc_Ntk_t * pNtk, float FiMin, float FiMax, float Delta, int fVerbose ) { - int Median; + float Median; assert( FiMin < FiMax ); - if ( FiMin + 1 == FiMax ) + if ( FiMin + Delta >= FiMax ) return FiMax; Median = FiMin + (FiMax - FiMin)/2; - if ( Seq_RetimeForPeriod( pNtk, Median, fVerbose ) ) - return Seq_RetimeSearch_rec( pNtk, FiMin, Median, fVerbose ); // Median is feasible + if ( Seq_NtkMappingForPeriod( pNtk, Median, fVerbose ) ) + return Seq_NtkMappingSearch_rec( pNtk, FiMin, Median, Delta, fVerbose ); // Median is feasible else - return Seq_RetimeSearch_rec( pNtk, Median, FiMax, fVerbose ); // Median is infeasible + return Seq_NtkMappingSearch_rec( pNtk, Median, FiMax, Delta, fVerbose ); // Median is infeasible } /**Function************************************************************* @@ -148,78 +144,63 @@ int Seq_RetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose ) +int Seq_NtkMappingForPeriod( Abc_Ntk_t * pNtk, float Fi, int fVerbose ) { Abc_Seq_t * p = pNtk->pManFunc; + Vec_Ptr_t * vLeaves, * vDelays; Abc_Obj_t * pObj; - int nMaxSteps = 10; int i, c, RetValue, fChange, Counter; char * pReason = ""; // set l-values of all nodes to be minus infinity - Vec_IntFill( p->vLValues, p->nSize, -ABC_INFINITY ); + Vec_IntFill( p->vLValues, p->nSize, -ABC_INFINITY ); // set l-values of constants and PIs pObj = Abc_NtkObj( pNtk, 0 ); - Seq_NodeSetLValue( pObj, 0 ); + Seq_NodeSetLValueP( pObj, 0.0 ); Abc_NtkForEachPi( pNtk, pObj, i ) - Seq_NodeSetLValue( pObj, 0 ); + Seq_NodeSetLValueP( pObj, 0.0 ); // update all values iteratively Counter = 0; - for ( c = 0; c < nMaxSteps; c++ ) + for ( c = 0; c < p->nMaxIters; c++ ) { fChange = 0; - Abc_AigForEachAnd( pNtk, pObj, i ) + Vec_PtrForEachEntry( p->vMapAnds, pObj, i ) { - if ( Seq_NodeCutMan(pObj) ) - RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi ); - else - RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi ); -//printf( "Node = %d. Value = %d. \n", pObj->Id, RetValue ); Counter++; - if ( RetValue == SEQ_UPDATE_FAIL ) - break; - if ( RetValue == SEQ_UPDATE_NO ) - continue; - fChange = 1; + vLeaves = Vec_VecEntry( p->vMapCuts, i ); + vDelays = Vec_VecEntry( p->vMapDelays, i ); + RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, vLeaves, vDelays ); + if ( RetValue == SEQ_UPDATE_YES ) + fChange = 1; } Abc_NtkForEachPo( pNtk, pObj, i ) { - if ( Seq_NodeCutMan(pObj) ) - RetValue = Seq_FpgaNodeUpdateLValue( pObj, Fi ); - else - RetValue = Seq_RetimeNodeUpdateLValue( pObj, Fi ); -//printf( "Node = %d. Value = %d. \n", pObj->Id, RetValue ); - Counter++; + RetValue = Seq_NtkNodeUpdateLValue( pObj, Fi, NULL, NULL ); if ( RetValue == SEQ_UPDATE_FAIL ) break; - if ( RetValue == SEQ_UPDATE_NO ) - continue; - fChange = 1; } if ( RetValue == SEQ_UPDATE_FAIL ) break; if ( fChange == 0 ) break; } - if ( c == nMaxSteps ) + if ( c == p->nMaxIters ) { RetValue = SEQ_UPDATE_FAIL; pReason = "(timeout)"; } - -//Abc_NtkForEachObj( pNtk, pObj, i ) -//printf( "%d ", Seq_NodeGetLValue(pObj) ); -//printf( "\n" ); + else + c++; // report the results if ( fVerbose ) { if ( RetValue == SEQ_UPDATE_FAIL ) - printf( "Period = %3d. Iterations = %3d. Updates = %10d. Infeasible %s\n", Fi, c, Counter, pReason ); + printf( "Period = %6.2f. Iterations = %3d. Updates = %10d. Infeasible %s\n", Fi, c, Counter, pReason ); else - printf( "Period = %3d. Iterations = %3d. Updates = %10d. Feasible\n", Fi, c, Counter ); + printf( "Period = %6.2f. Iterations = %3d. Updates = %10d. Feasible\n", Fi, c, Counter ); } return RetValue != SEQ_UPDATE_FAIL; } @@ -235,27 +216,66 @@ int Seq_RetimeForPeriod( Abc_Ntk_t * pNtk, int Fi, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Seq_RetimeNodeUpdateLValue( Abc_Obj_t * pObj, int Fi ) +int Seq_NtkNodeUpdateLValue( Abc_Obj_t * pObj, float Fi, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vDelays ) { - int lValueNew, lValueOld, lValue0, lValue1; + Abc_Seq_t * p = pObj->pNtk->pManFunc; + float lValueOld, lValueNew, lValueCur, lValuePin; + unsigned SeqEdge; + Abc_Obj_t * pLeaf; + int i; + assert( !Abc_ObjIsPi(pObj) ); assert( Abc_ObjFaninNum(pObj) > 0 ); - lValue0 = Seq_NodeGetLValue(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj); + // consider the case of the PO if ( Abc_ObjIsPo(pObj) ) - return (lValue0 > Fi)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO; - if ( Abc_ObjFaninNum(pObj) == 2 ) - lValue1 = Seq_NodeGetLValue(Abc_ObjFanin1(pObj)) - Fi * Seq_ObjFaninL1(pObj); - else - lValue1 = -ABC_INFINITY; - lValueNew = 1 + ABC_MAX( lValue0, lValue1 ); - lValueOld = Seq_NodeGetLValue(pObj); -// if ( lValueNew == lValueOld ) - if ( lValueNew <= lValueOld ) + { + lValueCur = Seq_NodeGetLValueP(Abc_ObjFanin0(pObj)) - Fi * Seq_ObjFaninL0(pObj); + return (lValueCur > Fi + p->fEpsilon)? SEQ_UPDATE_FAIL : SEQ_UPDATE_NO; + } + // get the new arrival time of the cut output + lValueNew = -ABC_INFINITY; + Vec_PtrForEachEntry( vLeaves, pLeaf, i ) + { + SeqEdge = (unsigned)pLeaf; + pLeaf = Abc_NtkObj( pObj->pNtk, SeqEdge >> 8 ); + lValueCur = Seq_NodeGetLValueP(pLeaf) - Fi * (SeqEdge & 255); + lValuePin = Abc_Int2Float( (int)Vec_PtrEntry(vDelays, i) ); + if ( lValueNew < lValuePin + lValueCur ) + lValueNew = lValuePin + lValueCur; + } + // compare + lValueOld = Seq_NodeGetLValueP( pObj ); + if ( lValueNew <= lValueOld + p->fEpsilon ) return SEQ_UPDATE_NO; - Seq_NodeSetLValue( pObj, lValueNew ); + // update the values + if ( lValueNew > lValueOld + p->fEpsilon ) + Seq_NodeSetLValueP( pObj, lValueNew ); return SEQ_UPDATE_YES; } + + +/**Function************************************************************* + + Synopsis [Add sequential edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NodeRetimeSetLag_rec( Abc_Obj_t * pNode, char Lag ) +{ + if ( pNode->pCopy ) + return; + Seq_NodeRetimeSetLag_rec( Abc_ObjFanin0(pNode), Lag ); + Seq_NodeRetimeSetLag_rec( Abc_ObjFanin1(pNode), Lag ); + Seq_NodeSetLag( pNode, Lag ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/seq/seqShare.c b/src/base/seq/seqShare.c index 818dca23..5f5f1731 100644 --- a/src/base/seq/seqShare.c +++ b/src/base/seq/seqShare.c @@ -160,8 +160,188 @@ void Seq_NodeShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNode Abc_ObjPatchFanin( pFanout, pNode, pBuffer ); } + + + + +/**Function************************************************************* + + Synopsis [Maps virtual latches into real latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Seq_NtkShareLatchesKey( Abc_Obj_t * pObj, Abc_InitType_t Init ) +{ + return (pObj->Id << 2) | Init; +} + +/**Function************************************************************* + + Synopsis [Maps virtual latches into real latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Seq_NtkShareLatches_rec( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj, Seq_Lat_t * pRing, int nLatch, stmm_table * tLatchMap ) +{ + Abc_Obj_t * pLatch, * pFanin; + Abc_InitType_t Init; + unsigned Key; + if ( nLatch == 0 ) + return pObj; + assert( pRing->pLatch == NULL ); + // get the latch on the previous level + pFanin = Seq_NtkShareLatches_rec( pNtk, pObj, Seq_LatNext(pRing), nLatch - 1, tLatchMap ); + + // get the initial state + Init = Seq_LatInit( pRing ); + // check if the latch with this initial state exists + Key = Seq_NtkShareLatchesKey( pFanin, Init ); + if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) ) + return pRing->pLatch = pLatch; + + // does not exist + if ( Init != ABC_INIT_DC ) + { + // check if the don't-care exists + Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_DC ); + if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) ) // yes + { + // update the table + stmm_delete( tLatchMap, (char **)&Key, (char **)&pLatch ); + Key = Seq_NtkShareLatchesKey( pFanin, Init ); + stmm_insert( tLatchMap, (char *)Key, (char *)pLatch ); + // change don't-care to the given value + pLatch->pData = (void *)Init; + return pRing->pLatch = pLatch; + } + + // add the latch with this value + pLatch = Abc_NtkCreateLatch( pNtk ); + pLatch->pData = (void *)Init; + Abc_ObjAddFanin( pLatch, pFanin ); + // add it to the table + Key = Seq_NtkShareLatchesKey( pFanin, Init ); + stmm_insert( tLatchMap, (char *)Key, (char *)pLatch ); + return pRing->pLatch = pLatch; + } + // the init value is the don't-care + + // check if care values exist + Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_ZERO ); + if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) ) + { + Seq_LatSetInit( pRing, ABC_INIT_ZERO ); + return pRing->pLatch = pLatch; + } + Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_ONE ); + if ( stmm_lookup( tLatchMap, (char *)Key, (char **)&pLatch ) ) + { + Seq_LatSetInit( pRing, ABC_INIT_ONE ); + return pRing->pLatch = pLatch; + } + + // create the don't-care latch + pLatch = Abc_NtkCreateLatch( pNtk ); + pLatch->pData = (void *)ABC_INIT_DC; + Abc_ObjAddFanin( pLatch, pFanin ); + // add it to the table + Key = Seq_NtkShareLatchesKey( pFanin, ABC_INIT_DC ); + stmm_insert( tLatchMap, (char *)Key, (char *)pLatch ); + return pRing->pLatch = pLatch; +} + +/**Function************************************************************* + + Synopsis [Maps virtual latches into real latches.] + + Description [Creates new latches and assigns them to virtual latches + on the edges of a sequential AIG. The nodes of the new network should + be created before this procedure is called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NtkShareLatches( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + stmm_table * tLatchMap; + int i; + assert( Abc_NtkIsSeq( pNtk ) ); + tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash ); + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap ); + Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin1(pObj)->pCopy, Seq_NodeGetRing(pObj,1), Seq_NodeCountLats(pObj,1), tLatchMap ); + } + Abc_NtkForEachPo( pNtk, pObj, i ) + Seq_NtkShareLatches_rec( pNtkNew, Abc_ObjFanin0(pObj)->pCopy, Seq_NodeGetRing(pObj,0), Seq_NodeCountLats(pObj,0), tLatchMap ); + stmm_free_table( tLatchMap ); +} + +/**Function************************************************************* + + Synopsis [Maps virtual latches into real latches.] + + Description [Creates new latches and assigns them to virtual latches + on the edges of a sequential AIG. The nodes of the new network should + be created before this procedure is called.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Seq_NtkShareLatchesFpga( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapAnds ) +{ + Abc_Obj_t * pObj, * pFanout; + stmm_table * tLatchMap; + int i, k, nOldNodes; + assert( Abc_NtkIsSeq( pNtk ) ); + // start the table + tLatchMap = stmm_init_table( stmm_ptrcmp, stmm_ptrhash ); + // remember the old nodes + nOldNodes = Vec_PtrSize( vMapAnds ); + // add constant and PIs + Vec_PtrPush( vMapAnds, Abc_NtkConst1(pNtk) ); + Abc_NtkForEachPi( pNtk, pObj, i ) + Vec_PtrPush( vMapAnds, pObj ); + // process nodes used in the mapping + Vec_PtrForEachEntry( vMapAnds, pObj, i ) + { + // make sure the label is clean + Abc_ObjForEachFanout( pObj, pFanout, k ) + assert( pFanout->fMarkC == 0 ); + Abc_ObjForEachFanout( pObj, pFanout, k ) + { + if ( pFanout->fMarkC ) + continue; + pFanout->fMarkC = 1; + if ( Abc_ObjFaninId0(pFanout) == pObj->Id ) + Seq_NtkShareLatches_rec( pNtkNew, pObj->pCopy, Seq_NodeGetRing(pFanout,0), Seq_NodeCountLats(pFanout,0), tLatchMap ); + if ( Abc_ObjFaninId1(pFanout) == pObj->Id ) + Seq_NtkShareLatches_rec( pNtkNew, pObj->pCopy, Seq_NodeGetRing(pFanout,1), Seq_NodeCountLats(pFanout,1), tLatchMap ); + } + // clean the label + Abc_ObjForEachFanout( pObj, pFanout, k ) + pFanout->fMarkC = 0; + } + stmm_free_table( tLatchMap ); + // return to the old array + Vec_PtrShrink( vMapAnds, nOldNodes ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c index b126b043..a3b8bc84 100644 --- a/src/base/seq/seqUtil.c +++ b/src/base/seq/seqUtil.c @@ -39,6 +39,37 @@ SeeAlso [] ***********************************************************************/ +int Seq_NtkLevelMax( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i, Result; + assert( Abc_NtkIsSeq(pNtk) ); + Result = 0; + Abc_NtkForEachPo( pNtk, pNode, i ) + { + pNode = Abc_ObjFanin0(pNode); + if ( Result < (int)pNode->Level ) + Result = pNode->Level; + } + Abc_SeqForEachCutsetNode( pNtk, pNode, i ) + { + if ( Result < (int)pNode->Level ) + Result = pNode->Level; + } + return Result; +} + +/**Function************************************************************* + + Synopsis [Returns the maximum latch number on any of the fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Seq_ObjFanoutLMax( Abc_Obj_t * pObj ) { Abc_Obj_t * pFanout; @@ -363,6 +394,29 @@ int Seq_NtkLatchGetEqualFaninNum( Abc_Ntk_t * pNtk ) return Counter; } +/**Function************************************************************* + + Synopsis [Returns the maximum latch number on any of the fanouts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Seq_NtkCountNodesAboveLimit( Abc_Ntk_t * pNtk, int Limit ) +{ + Abc_Obj_t * pNode; + int i, Counter; + assert( !Abc_NtkIsSeq(pNtk) ); + Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( Abc_ObjFaninNum(pNode) > Limit ) + Counter++; + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/fpga/fpga.c b/src/map/fpga/fpga.c index 2f399e6e..68b5f124 100644 --- a/src/map/fpga/fpga.c +++ b/src/map/fpga/fpga.c @@ -57,8 +57,8 @@ void Fpga_Init( Abc_Frame_t * pAbc ) { // set the default library //Fpga_LutLib_t s_LutLib = { "lutlib", 6, {0,1,2,4,8,16,32}, {0,1,2,3,4,5,6} }; - //Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} }; - Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} }; + Fpga_LutLib_t s_LutLib = { "lutlib", 5, {0,1,1,1,1,1}, {0,1,1,1,1,1} }; + //Fpga_LutLib_t s_LutLib = { "lutlib", 4, {0,1,1,1,1}, {0,1,1,1,1} }; //Fpga_LutLib_t s_LutLib = { "lutlib", 3, {0,1,1,1}, {0,1,1,1} }; Abc_FrameSetLibLut( Fpga_LutLibDup(&s_LutLib) ); diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c index 3f0e3134..9656b0f5 100644 --- a/src/map/mapper/mapperTree.c +++ b/src/map/mapper/mapperTree.c @@ -439,6 +439,9 @@ int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate ) pGate->tDelayMax.Fall = pGate->tDelaysF[k].Rise; if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Fall ) pGate->tDelayMax.Fall = pGate->tDelaysF[k].Fall; + + pGate->tDelaysF[k].Worst = MAP_MAX( pGate->tDelaysF[k].Fall, pGate->tDelaysF[k].Rise ); + pGate->tDelaysR[k].Worst = MAP_MAX( pGate->tDelaysR[k].Fall, pGate->tDelaysR[k].Rise ); } // count gates and area of the supergate diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index 307cdd8d..0e2c085d 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -90,6 +90,7 @@ extern float Mio_LibraryReadDelayInvMax( Mio_Library_t * pLib ); extern float Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib ); extern float Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib ); extern float Mio_LibraryReadDelayNand2Max( Mio_Library_t * pLib ); +extern float Mio_LibraryReadDelayAnd2Max( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaInv ( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaBuf ( Mio_Library_t * pLib ); extern float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ); diff --git a/src/map/mio/mioApi.c b/src/map/mio/mioApi.c index 90a0af93..a9aaac19 100644 --- a/src/map/mio/mioApi.c +++ b/src/map/mio/mioApi.c @@ -53,6 +53,7 @@ float Mio_LibraryReadDelayInvMax ( Mio_Library_t * pLib ) { retur float Mio_LibraryReadDelayNand2Rise( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockRise : 0.0); } float Mio_LibraryReadDelayNand2Fall( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockFall : 0.0); } float Mio_LibraryReadDelayNand2Max ( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->pPins->dDelayBlockMax : 0.0); } +float Mio_LibraryReadDelayAnd2Max ( Mio_Library_t * pLib ) { return (float)(pLib->pGateAnd2? pLib->pGateAnd2->pPins->dDelayBlockMax : 0.0); } float Mio_LibraryReadAreaInv ( Mio_Library_t * pLib ) { return (float)(pLib->pGateInv? pLib->pGateInv->dArea : 0.0); } float Mio_LibraryReadAreaBuf ( Mio_Library_t * pLib ) { return (float)(pLib->pGateBuf? pLib->pGateBuf->dArea : 0.0); } float Mio_LibraryReadAreaNand2 ( Mio_Library_t * pLib ) { return (float)(pLib->pGateNand2? pLib->pGateNand2->dArea : 0.0); } diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index 4f81a004..f5ecf9bd 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -29,7 +29,6 @@ #define inline __inline // compatible with MS VS 6.0 #endif -#include "vecFan.h" #include "vecInt.h" #include "vecStr.h" #include "vecPtr.h" diff --git a/src/misc/vec/vecFan.h b/src/misc/vec/vecFan_.h index 1493014a..1493014a 100644 --- a/src/misc/vec/vecFan.h +++ b/src/misc/vec/vecFan_.h diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 3c767f20..2d36addd 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -457,6 +457,41 @@ static inline void Vec_IntPush( Vec_Int_t * p, int Entry ) SeeAlso [] ***********************************************************************/ +static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry ) +{ + if ( p->nSize == p->nCap ) + { + int * pArray; + int i; + + if ( p->nSize == 0 ) + p->nCap = 1; + pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 ); +// pArray = ALLOC( int, p->nCap * 2 ); + if ( p->pArray ) + { + for ( i = 0; i < p->nSize; i++ ) + pArray[i] = p->pArray[i]; + Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 ); +// free( p->pArray ); + } + p->nCap *= 2; + p->pArray = pArray; + } + p->pArray[p->nSize++] = Entry; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry ) { int i; @@ -516,6 +551,26 @@ static inline int Vec_IntPop( Vec_Int_t * p ) /**Function************************************************************* + Synopsis [Find entry.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntFind( Vec_Int_t * p, int Entry ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + return i; + return -1; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -525,16 +580,19 @@ static inline int Vec_IntPop( Vec_Int_t * p ) SeeAlso [] ***********************************************************************/ -static inline void Vec_IntRemove( Vec_Int_t * p, int Entry ) +static inline int Vec_IntRemove( Vec_Int_t * p, int Entry ) { int i; for ( i = 0; i < p->nSize; i++ ) if ( p->pArray[i] == Entry ) break; + if ( i == p->nSize ) + return 0; assert( i < p->nSize ); for ( i++; i < p->nSize; i++ ) p->pArray[i-1] = p->pArray[i]; p->nSize--; + return 1; } /**Function************************************************************* diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h index f518e8c4..5c9b2e8e 100644 --- a/src/opt/cut/cut.h +++ b/src/opt/cut/cut.h @@ -69,6 +69,8 @@ struct Cut_CutStruct_t_ unsigned nVarsMax : 4; // the max number of vars [4-6] unsigned nLeaves : 4; // the number of leaves [4-6] unsigned uSign; // the signature + unsigned uCanon0; // the canonical form + unsigned uCanon1; // the canonical form Cut_Cut_t * pNext; // the next cut in the list int pLeaves[0]; // the array of leaves }; @@ -113,6 +115,7 @@ extern int Cut_ManReadVarsMax( Cut_Man_t * p ); /*=== cutNode.c ==========================================================*/ extern Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv ); extern Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes ); +extern Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst ); /*=== cutSeq.c ==========================================================*/ extern void Cut_NodeComputeCutsSeq( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int nLat0, int nLat1, int fTriv, int CutSetNum ); extern void Cut_NodeNewMergeWithOld( Cut_Man_t * p, int Node ); @@ -126,6 +129,8 @@ extern int Cut_OracleReadDrop( Cut_Oracle_t * p ); extern void Cut_OracleNodeSetTriv( Cut_Oracle_t * p, int Node ); extern Cut_Cut_t * Cut_OracleComputeCuts( Cut_Oracle_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 ); extern void Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node ); +/*=== cutTruth.c ==========================================================*/ +extern void Cut_TruthCanonicize( Cut_Cut_t * pCut ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c index 80568d71..0268ba19 100644 --- a/src/opt/cut/cutNode.c +++ b/src/opt/cut/cutNode.c @@ -376,6 +376,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC // start with the elementary cut if ( fTriv ) { +// printf( "Creating trivial cut %d.\n", Node ); pTemp0 = Cut_CutCreateTriv( p, Node ); Cut_ListAdd( pSuper, pTemp0 ); p->nNodeCuts++; @@ -542,6 +543,189 @@ p->timeUnion += clock() - clk; return pList; } +/**Function************************************************************* + + Synopsis [Computes the cuts by unioning cuts at a choice node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_NodeUnionCutsSeq( Cut_Man_t * p, Vec_Int_t * vNodes, int CutSetNum, int fFirst ) +{ + Cut_List_t Super, * pSuper = &Super; + Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop; + int i, k, Node, Root, Limit = p->pParams->nVarsMax; + int clk = clock(); + + // start the new list + Cut_ListStart( pSuper ); + + // remember the root node to save the resulting cuts + Root = Vec_IntEntry( vNodes, 0 ); + p->nNodeCuts = 1; + + // store the original lists for comparison + p->pCompareOld = Cut_NodeReadCutsOld( p, Root ); + p->pCompareNew = (CutSetNum >= 0)? Cut_NodeReadCutsNew( p, Root ) : NULL; + + // get the topmost cut + pTop = NULL; + if ( (pTop = Cut_NodeReadCutsOld( p, Root )) == NULL ) + pTop = Cut_NodeReadCutsNew( p, Root ); + assert( pTop != NULL ); + + // collect small cuts first + Vec_PtrClear( p->vTemp ); + Vec_IntForEachEntry( vNodes, Node, i ) + { + // get the cuts of this node + if ( i == 0 && CutSetNum >= 0 ) + { + pList = Cut_NodeReadCutsTemp( p, CutSetNum ); + Cut_NodeWriteCutsTemp( p, CutSetNum, NULL ); + } + else + { + pList = Cut_NodeReadCutsNew( p, Node ); + Cut_NodeWriteCutsNew( p, Node, NULL ); + } + if ( pList == NULL ) + continue; + + // process the cuts + if ( fFirst ) + { + // remember the starting point + pListStart = pList->pNext; + pList->pNext = NULL; + // save or recycle the elementary cut + if ( i == 0 ) + Cut_ListAdd( pSuper, pList ); + else + Cut_CutRecycle( p, pList ); + } + else + pListStart = pList; + + // save all the cuts that are smaller than the limit + Cut_ListForEachCutSafe( pListStart, pCut, pCut2 ) + { + if ( pCut->nLeaves == (unsigned)Limit ) + { + Vec_PtrPush( p->vTemp, pCut ); + break; + } + // check containment +// if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) ) +// continue; + if ( p->pParams->fFilter ) + { + if ( Cut_CutFilterOne(p, pSuper, pCut) ) + continue; + if ( p->pParams->fSeq ) + { + if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) ) + continue; + if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) ) + continue; + } + } + + // set the complemented bit by comparing the first cut with the current cut + pCut->fCompl = pTop->fSimul ^ pCut->fSimul; + pListStart = pCut->pNext; + pCut->pNext = NULL; + // add to the list + Cut_ListAdd( pSuper, pCut ); + if ( ++p->nNodeCuts == p->pParams->nKeepMax ) + { + // recycle the rest of the cuts of this node + Cut_ListForEachCutSafe( pListStart, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + // recycle all cuts of other nodes + Vec_IntForEachEntryStart( vNodes, Node, k, i+1 ) + Cut_NodeFreeCuts( p, Node ); + // recycle the saved cuts of other nodes + Vec_PtrForEachEntry( p->vTemp, pList, k ) + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + goto finish; + } + } + } + // collect larger cuts next + Vec_PtrForEachEntry( p->vTemp, pList, i ) + { + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + { + // check containment +// if ( p->pParams->fFilter && Cut_CutFilterOne( p, pSuper, pCut ) ) +// continue; + if ( p->pParams->fFilter ) + { + if ( Cut_CutFilterOne(p, pSuper, pCut) ) + continue; + if ( p->pParams->fSeq ) + { + if ( p->pCompareOld && Cut_CutFilterOld(p, p->pCompareOld, pCut) ) + continue; + if ( p->pCompareNew && Cut_CutFilterOld(p, p->pCompareNew, pCut) ) + continue; + } + } + + // set the complemented bit + pCut->fCompl = pTop->fSimul ^ pCut->fSimul; + pListStart = pCut->pNext; + pCut->pNext = NULL; + // add to the list + Cut_ListAdd( pSuper, pCut ); + if ( ++p->nNodeCuts == p->pParams->nKeepMax ) + { + // recycle the rest of the cuts + Cut_ListForEachCutSafe( pListStart, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + // recycle the saved cuts of other nodes + Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 ) + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + goto finish; + } + } + } +finish : + // set the cuts at the node + pList = Cut_ListFinish( pSuper ); + + // set the lists at the node +// assert( Cut_NodeReadCutsNew(p, Root) == NULL ); +// Cut_NodeWriteCutsNew( p, Root, pList ); + if ( CutSetNum >= 0 ) + { + assert( Cut_NodeReadCutsTemp(p, CutSetNum) == NULL ); + Cut_NodeWriteCutsTemp( p, CutSetNum, pList ); + } + else + { + assert( Cut_NodeReadCutsNew(p, Root) == NULL ); + Cut_NodeWriteCutsNew( p, Root, pList ); + } + +p->timeUnion += clock() - clk; + // filter the cuts +//clk = clock(); +// if ( p->pParams->fFilter ) +// Cut_CutFilter( p, pList ); +//p->timeFilter += clock() - clk; +// if ( fFirst ) +// p->nNodes -= vNodes->nSize - 1; + return pList; +} + /**Function************************************************************* diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c index 28984e5a..b65e5eff 100644 --- a/src/opt/cut/cutTruth.c +++ b/src/opt/cut/cutTruth.c @@ -107,6 +107,48 @@ void Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, i } } +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [This procedure cannot be used while recording oracle + because it will overwrite Num0 and Num1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TruthCanonicize( Cut_Cut_t * pCut ) +{ + unsigned uTruth; + unsigned * uCanon2; + char * pPhases2; + assert( pCut->nVarsMax < 6 ); + + // get the direct truth table + uTruth = *Cut_CutReadTruth(pCut); + + // compute the direct truth table + Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 ); +// uCanon[0] = uCanon2[0]; +// uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0]; +// uPhases[0] = pPhases2[0]; + pCut->uCanon0 = uCanon2[0]; + pCut->Num0 = pPhases2[0]; + + // get the complemented truth table + uTruth = ~*Cut_CutReadTruth(pCut); + + // compute the direct truth table + Extra_TruthCanonFastN( pCut->nVarsMax, pCut->nLeaves, &uTruth, &uCanon2, &pPhases2 ); +// uCanon[0] = uCanon2[0]; +// uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0]; +// uPhases[0] = pPhases2[0]; + pCut->uCanon1 = uCanon2[0]; + pCut->Num1 = pPhases2[0]; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h index aa2a7039..b6b2524b 100644 --- a/src/opt/dec/dec.h +++ b/src/opt/dec/dec.h @@ -96,6 +96,7 @@ struct Dec_Man_t_ /*=== decAbc.c ========================================================*/ extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph ); +extern Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph ); extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain ); /*=== decFactor.c ========================================================*/ diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c index 6782a02f..1416cf0d 100644 --- a/src/opt/dec/decAbc.c +++ b/src/opt/dec/decAbc.c @@ -63,6 +63,44 @@ Abc_Obj_t * Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph ) /**Function************************************************************* + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph ) +{ + Abc_Obj_t * pAnd, * pAnd0, * pAnd1; + Dec_Node_t * pNode; + int i; + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Abc_ObjNotCond( Abc_NtkConst1(pNtk), Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + return Abc_ObjNotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph + Dec_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Abc_ObjNotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); +// pNode->pFunc = Abc_AigAnd( pNtk->pManFunc, pAnd0, pAnd1 ); + pAnd = Abc_NtkCreateNode( pNtk ); + Abc_ObjAddFanin( pAnd, pAnd0 ); + Abc_ObjAddFanin( pAnd, pAnd1 ); + pNode->pFunc = pAnd; + } + // complement the result if necessary + return Abc_ObjNotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + Synopsis [Counts the number of new nodes added when using this graph.] Description [AIG nodes for the fanins should be assigned to pNode->pFunc diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c index 24b86c95..02b7605c 100644 --- a/src/opt/fxu/fxuCreate.c +++ b/src/opt/fxu/fxuCreate.c @@ -24,11 +24,11 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder ); +static void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder ); static int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY ); static void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext ); static Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode ); -static Abc_Fan_t * s_pLits; +static int * s_pLits; extern int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax ); @@ -53,7 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) Fxu_Var * pVar; Fxu_Cube * pCubeFirst, * pCubeNew; Fxu_Cube * pCube1, * pCube2; - Vec_Fan_t * vFanins; + Vec_Int_t * vFanins; char * pSopCover; char * pSopCube; int * pOrder, nBitsMax; @@ -151,7 +151,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) pOrder[v] = v; // reorder the fanins qsort( (void *)pOrder, nFanins, sizeof(int),(int (*)(const void *, const void *))Fxu_CreateMatrixLitCompare); - assert( s_pLits[ pOrder[0] ].iFan < s_pLits[ pOrder[nFanins-1] ].iFan ); + assert( s_pLits[ pOrder[0] ] < s_pLits[ pOrder[nFanins-1] ] ); // create the corresponding cubes in the matrix pCubeFirst = NULL; c = 0; @@ -214,7 +214,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData ) SeeAlso [] ***********************************************************************/ -void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder ) +void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Int_t * vFanins, int * pOrder ) { Fxu_Var * pVar; int Value, i; @@ -224,12 +224,12 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Value = pSopCube[pOrder[i]]; if ( Value == '0' ) { - pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan + 1 ]; // CST + pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] + 1 ]; // CST Fxu_MatrixAddLiteral( p, pCube, pVar ); } else if ( Value == '1' ) { - pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]].iFan ]; // CST + pVar = p->ppVars[ 2 * vFanins->pArray[pOrder[i]] ]; // CST Fxu_MatrixAddLiteral( p, pCube, pVar ); } } @@ -409,7 +409,7 @@ Fxu_Cube * Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iV ***********************************************************************/ int Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY ) { - return s_pLits[*ptrX].iFan - s_pLits[*ptrY].iFan; + return s_pLits[*ptrX] - s_pLits[*ptrY]; } //////////////////////////////////////////////////////////////////////// |