diff options
| -rw-r--r-- | abc.dsp | 12 | ||||
| -rw-r--r-- | abc.opt | bin | 51712 -> 51712 bytes | |||
| -rw-r--r-- | abc.plg | 42 | ||||
| -rw-r--r-- | src/base/abc/abc.h | 34 | ||||
| -rw-r--r-- | src/base/abc/abcCheck.c | 7 | ||||
| -rw-r--r-- | src/base/abc/abcObj.c | 8 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 6 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/base/abcs/abcForBack.c | 161 | ||||
| -rw-r--r-- | src/base/abcs/abcLogic.c | 140 | ||||
| -rw-r--r-- | src/base/abcs/abcSeq.c | 648 | ||||
| -rw-r--r-- | src/base/abcs/abcUtils.c | 243 |
12 files changed, 726 insertions, 577 deletions
@@ -270,12 +270,24 @@ SOURCE=.\src\base\abci\abcVerify.c # PROP Default_Filter "" # Begin Source File +SOURCE=.\src\base\abcs\abcForBack.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\abcs\abcLogic.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abcs\abcRetime.c # End Source File # Begin Source File SOURCE=.\src\base\abcs\abcSeq.c # End Source File +# Begin Source File + +SOURCE=.\src\base\abcs\abcUtils.c +# End Source File # End Group # Begin Group "cmd" @@ -6,13 +6,13 @@ --------------------Configuration: abc - Win32 Debug-------------------- </h3> <h3>Command Lines</h3> -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1748.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1AD8.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\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\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\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\map\pga\pgaMan.c" +"C:\_projects\abc\src\base\abcs\abcLogic.c" ] -Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1748.tmp" -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1749.tmp" with contents +Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1AD8.tmp" +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1AD9.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 @@ -42,6 +42,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\abcMap.obj .\Debug\abcMiter.obj .\Debug\abcNtbdd.obj +.\Debug\abcPga.obj .\Debug\abcPrint.obj .\Debug\abcReconv.obj .\Debug\abcRefactor.obj @@ -270,6 +271,10 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\superAnd.obj .\Debug\superGate.obj .\Debug\superWrite.obj +.\Debug\pgaCore.obj +.\Debug\pgaMan.obj +.\Debug\pgaMatch.obj +.\Debug\pgaUtil.obj .\Debug\extraBddMisc.obj .\Debug\extraBddSymm.obj .\Debug\extraUtilBitMatrix.obj @@ -305,18 +310,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32 .\Debug\mvcPrint.obj .\Debug\mvcSort.obj .\Debug\mvcUtils.obj -.\Debug\pgaMan.obj -.\Debug\pgaUtil.obj -.\Debug\pgaMatch.obj -.\Debug\pgaCore.obj -.\Debug\abcPga.obj +.\Debug\abcLogic.obj +.\Debug\abcUtils.obj +.\Debug\abcForBack.obj ] -Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1749.tmp" +Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1AD9.tmp" <h3>Output Window</h3> Compiling... -pgaMan.c +abcLogic.c Linking... -Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp" with contents +Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1ADA.tmp" with contents [ /nologo /o"Debug/abc.bsc" .\Debug\abcAig.sbr @@ -346,6 +349,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp" with cont .\Debug\abcMap.sbr .\Debug\abcMiter.sbr .\Debug\abcNtbdd.sbr +.\Debug\abcPga.sbr .\Debug\abcPrint.sbr .\Debug\abcReconv.sbr .\Debug\abcRefactor.sbr @@ -574,6 +578,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp" with cont .\Debug\superAnd.sbr .\Debug\superGate.sbr .\Debug\superWrite.sbr +.\Debug\pgaCore.sbr +.\Debug\pgaMan.sbr +.\Debug\pgaMatch.sbr +.\Debug\pgaUtil.sbr .\Debug\extraBddMisc.sbr .\Debug\extraBddSymm.sbr .\Debug\extraUtilBitMatrix.sbr @@ -609,12 +617,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp" with cont .\Debug\mvcPrint.sbr .\Debug\mvcSort.sbr .\Debug\mvcUtils.sbr -.\Debug\pgaMan.sbr -.\Debug\pgaUtil.sbr -.\Debug\pgaMatch.sbr -.\Debug\pgaCore.sbr -.\Debug\abcPga.sbr] -Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP174A.tmp" +.\Debug\abcLogic.sbr +.\Debug\abcUtils.sbr +.\Debug\abcForBack.sbr] +Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1ADA.tmp" Creating browse info file... <h3>Output Window</h3> diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 0e296d64..02b284e6 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -169,6 +169,8 @@ struct Abc_Ntk_t_ Vec_Ptr_t * vSupps; // the satisfiable assignment of the miter int * pModel; + // initial states + Vec_Int_t * vInits; // the external don't-care if given Abc_Ntk_t * pExdc; // the EXDC network // miscellaneous data members @@ -305,6 +307,7 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj ) { return Ab 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 Abc_Obj_t * Abc_ObjGetCopy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjRegular(pObj)->pCopy, Abc_ObjIsComplement(pObj) ); } static inline Abc_Obj_t * Abc_ObjFanoutFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) { assert( !Abc_NtkIsLogic(pObj->pNtk) ); return (Abc_ObjFaninId0(pFanout) == (int)pObj->Id)? Abc_ObjChild0(pFanout) : Abc_ObjChild1(pFanout); } 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; } @@ -319,6 +322,8 @@ extern void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFano extern void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ); extern int Abc_ObjFanoutLMin( Abc_Obj_t * pObj ); extern int Abc_ObjFanoutLMax( Abc_Obj_t * pObj ); +extern int Abc_ObjFanoutLSum( Abc_Obj_t * pObj ); +extern int Abc_ObjFaninLSum( Abc_Obj_t * pObj ); // checking the node type static inline bool Abc_NodeIsAigAnd( Abc_Obj_t * pNode ) { assert(Abc_NtkHasAig(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2; } @@ -337,12 +342,13 @@ static inline bool Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode ) { r static inline bool Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode ) { return (bool)(pNode->TravId == pNode->pNtk->nTravIds - 1); } // checking initial state of the latches -static inline void Abc_LatchSetInit0( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)0; } -static inline void Abc_LatchSetInit1( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)1; } -static inline void Abc_LatchSetInitDc( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)2; } +static inline void Abc_LatchSetInit0( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)0; } +static inline void Abc_LatchSetInit1( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)1; } +static inline void Abc_LatchSetInitDc( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)2; } static inline bool Abc_LatchIsInit0( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)0; } static inline bool Abc_LatchIsInit1( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)1; } static inline bool Abc_LatchIsInitDc( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)2; } +static inline int Abc_LatchInit( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData; } // outputs the runtime in seconds #define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) @@ -364,6 +370,12 @@ static inline bool Abc_LatchIsInitDc( Abc_Obj_t * pLatch ) { assert(Abc #define Abc_NtkForEachLatch( pNtk, pObj, i ) \ for ( i = 0; i < Vec_PtrSize(pNtk->vLats); i++ ) \ if ( pObj = Abc_NtkLatch(pNtk, i) ) +#define Abc_AigForEachAnd( pNtk, pNode, i ) \ + for ( i = 0; i < Vec_PtrSize(pNtk->vObjs); i++ ) \ + if ( (pNode = Abc_NtkObj(pNtk, i)) && Abc_NodeIsAigAnd(pNode) ) +#define Abc_SeqForEachCutsetNode( pNtk, pNode, i ) \ + for ( i = 0; i < Vec_PtrSize(pNtk->vLats); i++ ) \ + if ( (pNode = Abc_NtkLatch(pNtk, i)) ) // inputs and outputs #define Abc_NtkForEachPi( pNtk, pPi, i ) \ for ( i = 0; (i < Abc_NtkPiNum(pNtk)) && (((pPi) = Abc_NtkPi(pNtk, i)), 1); i++ ) @@ -529,6 +541,7 @@ extern void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk ); /*=== abcNtk.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); +extern Abc_Ntk_t * Abc_NtkStartFromSeq( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func ); extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ); @@ -572,13 +585,20 @@ extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pN /*=== abcSat.c ==========================================================*/ extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ); -/*=== abcSeq.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ); -extern int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk ); + +/*=== abcForBack.c ==========================================================*/ extern void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk ); extern void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk ); +/*=== abcLogic.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ); +/*=== abcRetime.c ==========================================================*/ extern void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk ); +/*=== abcSeq.c ==========================================================*/ +extern Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ); +/*=== abcUtil.c ==========================================================*/ +extern int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk ); +extern int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk ); + /*=== abcSop.c ==========================================================*/ extern char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName ); extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars ); diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 356a4eba..b91a1291 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -160,9 +160,10 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ) } // check the latches - Abc_NtkForEachLatch( pNtk, pNode, i ) - if ( !Abc_NtkCheckLatch( pNtk, pNode ) ) - return 0; + if ( !Abc_NtkIsSeq(pNtk) ) + Abc_NtkForEachLatch( pNtk, pNode, i ) + if ( !Abc_NtkCheckLatch( pNtk, pNode ) ) + return 0; // finally, check for combinational loops // clk = clock(); diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 53ba3568..eddfd8b8 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -186,8 +186,8 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ) { Abc_Obj_t * pConst1; - assert( Abc_NtkIsStrash(pNtkAig) ); - assert( Abc_NtkIsSopLogic(pNtkNew) ); + assert( Abc_NtkHasAig(pNtkAig) ); + assert( Abc_NtkIsLogic(pNtkNew) ); pConst1 = Abc_AigConst1(pNtkAig->pManFunc); if ( Abc_ObjFanoutNum(pConst1) > 0 ) pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew ); @@ -208,8 +208,8 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ) Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ) { Abc_Obj_t * pReset, * pConst1; - assert( Abc_NtkIsStrash(pNtkAig) ); - assert( Abc_NtkIsSopLogic(pNtkNew) ); + assert( Abc_NtkHasAig(pNtkAig) ); + assert( Abc_NtkIsLogic(pNtkNew) ); pReset = Abc_AigReset(pNtkAig->pManFunc); if ( Abc_ObjFanoutNum(pReset) > 0 ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c4feb7a2..f2cfaaf1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3939,6 +3939,12 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( Abc_NtkCountSelfFeedLatches(pNtk) ) + { + fprintf( pErr, "Works AIG has self-feeding latches. Cannot continue.\n" ); + return 1; + } + // get the new network pNtkRes = Abc_NtkAigToSeq( pNtk ); if ( pNtkRes == NULL ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 41b9288e..e4af8e12 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -50,7 +50,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) if ( !Abc_NtkIsSeq(pNtk) ) fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) ); else - fprintf( pFile, " lat = %4d", Abc_NtkSeqLatchNum(pNtk) ); + fprintf( pFile, " lat = %4d(%d)", Abc_NtkSeqLatchNum(pNtk), Abc_NtkSeqLatchNumShared(pNtk) ); if ( Abc_NtkIsNetlist(pNtk) ) { diff --git a/src/base/abcs/abcForBack.c b/src/base/abcs/abcForBack.c new file mode 100644 index 00000000..4db162e1 --- /dev/null +++ b/src/base/abcs/abcForBack.c @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [abcForBack.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Simple forward/backward retiming procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcForBack.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs forward retiming of the sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode, * pFanout; + int i, k, nLatches; + assert( Abc_NtkIsSeq( pNtk ) ); + // assume that all nodes can be retimed + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + Vec_PtrPush( vNodes, pNode ); + pNode->fMarkA = 1; + } + // process the nodes + Vec_PtrForEachEntry( vNodes, pNode, i ) + { +// printf( "(%d,%d) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) ); + // get the number of latches to retime + nLatches = Abc_ObjFaninLMin(pNode); + if ( nLatches == 0 ) + continue; + assert( nLatches > 0 ); + // subtract these latches on the fanin side + Abc_ObjAddFaninL0( pNode, -nLatches ); + Abc_ObjAddFaninL1( pNode, -nLatches ); + // add these latches on the fanout size + Abc_ObjForEachFanout( pNode, pFanout, k ) + { + Abc_ObjAddFanoutL( pNode, pFanout, nLatches ); + if ( pFanout->fMarkA == 0 ) + { // schedule the node for updating + Vec_PtrPush( vNodes, pFanout ); + pFanout->fMarkA = 1; + } + } + // unmark the node as processed + pNode->fMarkA = 0; + } + Vec_PtrFree( vNodes ); + // clean the marks + Abc_NtkForEachNode( pNtk, pNode, i ) + { + pNode->fMarkA = 0; + if ( Abc_NodeIsConst(pNode) ) + continue; + assert( Abc_ObjFaninLMin(pNode) == 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Performs forward retiming of the sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode, * pFanin, * pFanout; + int i, k, nLatches; + assert( Abc_NtkIsSeq( pNtk ) ); + // assume that all nodes can be retimed + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + continue; + Vec_PtrPush( vNodes, pNode ); + pNode->fMarkA = 1; + } + // process the nodes + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + // get the number of latches to retime + nLatches = Abc_ObjFanoutLMin(pNode); + if ( nLatches == 0 ) + continue; + assert( nLatches > 0 ); + // subtract these latches on the fanout side + Abc_ObjForEachFanout( pNode, pFanout, k ) + Abc_ObjAddFanoutL( pNode, pFanout, -nLatches ); + // add these latches on the fanin size + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + Abc_ObjAddFaninL( pNode, k, nLatches ); + if ( Abc_ObjIsPi(pFanin) || Abc_NodeIsConst(pFanin) ) + continue; + if ( pFanin->fMarkA == 0 ) + { // schedule the node for updating + Vec_PtrPush( vNodes, pFanin ); + pFanin->fMarkA = 1; + } + } + // unmark the node as processed + pNode->fMarkA = 0; + } + Vec_PtrFree( vNodes ); + // clean the marks + Abc_NtkForEachNode( pNtk, pNode, i ) + { + pNode->fMarkA = 0; + if ( Abc_NodeIsConst(pNode) ) + continue; +// assert( Abc_ObjFanoutLMin(pNode) == 0 ); + } +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abcs/abcLogic.c b/src/base/abcs/abcLogic.c new file mode 100644 index 00000000..f33ed40e --- /dev/null +++ b/src/base/abcs/abcLogic.c @@ -0,0 +1,140 @@ +/**CFile**************************************************************** + + FileName [abcSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, int Init ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts a sequential AIG into a logic SOP network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pObjNew, * pFaninNew; + Vec_Ptr_t * vCutset; + char Buffer[100]; + int i, Init, nDigits; + assert( Abc_NtkIsSeq(pNtk) ); + // start the network + vCutset = pNtk->vLats; pNtk->vLats = Vec_PtrAlloc( 0 ); + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP ); + Vec_PtrFree( pNtk->vLats ); pNtk->vLats = vCutset; + // create the constant node + Abc_NtkDupConst1( pNtk, pNtkNew ); + // duplicate the nodes, create node functions and latches + Abc_AigForEachAnd( pNtk, pObj, i ) + { + Abc_NtkDupObj(pNtkNew, pObj); + pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + } + // connect the objects + Abc_AigForEachAnd( pNtk, pObj, i ) + { + // get the initial states of the latches on the fanin edge of this node + Init = Vec_IntEntry( pNtk->vInits, pObj->Id ); + // create the edge + pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninL0(pObj), Init & 0xFFFF ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + // create the edge + pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Abc_ObjFaninL1(pObj), Init >> 16 ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + // the complemented edges are subsumed by node function + } + // set the complemented attributed of CO edges (to be fixed by making simple COs) + Abc_NtkForEachPo( pNtk, pObj, i ) + { + // get the initial states of the latches on the fanin edge of this node + Init = Vec_IntEntry( pNtk->vInits, pObj->Id ); + // create the edge + pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninL0(pObj), Init & 0xFFFF ); + Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); + // create the complemented edge + if ( Abc_ObjFaninC0(pObj) ) + Abc_ObjSetFaninC( pObj->pCopy, 0 ); + } + // count the number of digits in the latch names + nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) ); + // add the latches and their names + Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) + { + // add the latch to the CI/CO arrays + Vec_PtrPush( pNtkNew->vCis, pObjNew ); + Vec_PtrPush( pNtkNew->vCos, pObjNew ); + // create latch name + sprintf( Buffer, "L%0*d", nDigits, i ); + Abc_NtkLogicStoreName( pObjNew, Buffer ); + } + // fix the problem with complemented and duplicated CO edges + Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); + // duplicate the EXDC network + if ( pNtk->pExdc ) + fprintf( stdout, "Warning: EXDC network is not copied.\n" ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" ); + return pNtkNew; +} + + +/**Function************************************************************* + + Synopsis [Creates latches on one edge.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, int Init ) +{ + Abc_Obj_t * pLatch; + if ( nLatches == 0 ) + return pFanin->pCopy; + pFanin = Abc_NodeSeqToLogic( pNtkNew, pFanin, nLatches - 1, Init >> 2 ); + pLatch = Abc_NtkCreateLatch( pNtkNew ); + pLatch->pData = (void *)(Init & 3); + Abc_ObjAddFanin( pLatch, pFanin ); + return pLatch; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c index 344417af..eca337fd 100644 --- a/src/base/abcs/abcSeq.c +++ b/src/base/abcs/abcSeq.c @@ -6,7 +6,7 @@ PackageName [Network and node package.] - Synopsis [] + Synopsis [Procedures to derive sequential AIG from combinational AIG with latches.] Author [Alan Mishchenko] @@ -21,27 +21,32 @@ #include "abc.h" /* - A sequential network is an AIG whose edges have number-of-latches attributes, - in addition to the complemented attibutes. - - The sets of PIs/POs remain the same as in logic network. - Constant 1 node can only be used as a fanin of a PO node and the reset node. - The reset node produces sequence (01111...). It is used to create the - initialization logic of all latches. - The latches do not have explicit initial state but they are implicitly - reset by the reset node. - + A sequential network is similar to AIG in that it contains only + AND gates. However, the AND-gates are currently not hashed. + Const1/PIs/POs remain the same as in the original AIG. + Instead of the latches, a new cutset is added, which is currently + defined as a set of AND gates that have a latch among their fanouts. + The edges of a sequential AIG are labeled with latch attributes + in addition to the complementation attibutes. + The attributes contain information about the number of latches + and their initial states. + The number of latches is stored directly on the edges. The initial + states are stored in a special array associated with the network. + The AIG of sequential network is static in the sense that the + new AIG nodes are never created. + The retiming (or retiming/mapping) is performed by moving the + latches over the static nodes of the AIG. + The new initial state after forward retiming is computed in a + straight-forward manner. After backward retiming it is computed + by setting up a SAT problem. */ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Vec_Int_t * Abc_NtkSeqCountLatches( Abc_Ntk_t * pNtk ); -static void Abc_NodeSeqCountLatches( Abc_Obj_t * pObj, Vec_Int_t * vNumbers ); - -static void Abc_NtkSeqCreateLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); -static void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches ); +static Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk ); +static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pAnd, int Num, int * pnLatches, int * pnInit ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -51,7 +56,9 @@ static void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches ); Synopsis [Converts a normal AIG into a sequential AIG.] - Description [] + Description [The const/PI/PO nodes are duplicated. The internal + nodes are duplicated in the topological order. The dangling nodes + are not copies. The choice nodes are copied.] SideEffects [] @@ -61,119 +68,62 @@ static void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches ); Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) { Abc_Ntk_t * pNtkNew; - Abc_Aig_t * pManNew; Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj, * pConst, * pFanout, * pFaninNew, * pLatch; - int i, k, fChange, Counter; - + Abc_Obj_t * pObj, * pFanin0, * pFanin1; + int i, nLatches0, nLatches1, Init0, Init1; + // make sure it is an AIG without self-feeding latches assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 ); // start the network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_SEQ, ABC_FUNC_AIG ); - pManNew = pNtkNew->pManFunc; - - // set mapping of the constant nodes - Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1( pManNew ); - Abc_AigReset(pNtk->pManFunc)->pCopy = Abc_AigReset( pManNew ); - - // get rid of initial states - Abc_NtkForEachLatch( pNtk, pObj, i ) - { - pObj->pNext = pObj->pCopy; - if ( Abc_LatchIsInit0(pObj) ) - pObj->pCopy = Abc_AigAnd( pManNew, pObj->pCopy, Abc_AigReset(pManNew) ); - else if ( Abc_LatchIsInit1(pObj) ) - pObj->pCopy = Abc_AigOr( pManNew, pObj->pCopy, Abc_ObjNot( Abc_AigReset(pManNew) ) ); - } - - // copy internal nodes - vNodes = Abc_AigDfs( pNtk, 1, 0 ); + pNtkNew = Abc_NtkAlloc( ABC_TYPE_SEQ, ABC_FUNC_AIG ); + // duplicate the name and the spec + pNtkNew->pName = util_strsav(pNtk->pName); + pNtkNew->pSpec = util_strsav(pNtk->pSpec); + // clone const/PIs/POs + Abc_NtkDupObj(pNtkNew, Abc_AigConst1(pNtk->pManFunc) ); + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkDupObj(pNtkNew, pObj); + // copy the PI/PO names + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pObj) ); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pObj) ); + // copy the internal nodes, including choices, excluding dangling + vNodes = Abc_AigDfs( pNtk, 0, 0 ); Vec_PtrForEachEntry( vNodes, pObj, i ) - if ( Abc_ObjFaninNum(pObj) == 2 ) - pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + Abc_NtkDupObj(pNtkNew, pObj); Vec_PtrFree( vNodes ); - - // relink the CO nodes - Abc_NtkForEachPo( pNtk, pObj, i ) - Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjAddFanin( pObj->pNext, Abc_ObjChild0Copy(pObj) ); - - // propagate constant input latches in the new network - Counter = 0; - fChange = 1; - while ( fChange ) + // start the storage for initial states + pNtkNew->vInits = Vec_IntStart( Abc_NtkObjNumMax(pNtkNew) ); + // reconnect the internal nodes + Abc_AigForEachAnd( pNtk, pObj, i ) { - fChange = 0; - Abc_NtkForEachLatch( pNtkNew, pLatch, i ) - { - if ( Abc_ObjFanoutNum(pLatch) == 0 ) - continue; - pFaninNew = Abc_ObjFanin0(pLatch); - if ( Abc_ObjIsCi(pFaninNew) || !Abc_NodeIsConst(pFaninNew) ) - continue; - pConst = Abc_ObjNotCond( Abc_AigConst1(pManNew), Abc_ObjFaninC0(pLatch) ); - Abc_AigReplace( pManNew, pLatch, pConst, 0 ); - fChange = 1; - Counter++; - } + // process the fanins of the AND gate (pObj) + pFanin0 = Abc_NodeAigToSeq( pObj, 0, &nLatches0, &Init0 ); + pFanin1 = Abc_NodeAigToSeq( pObj, 1, &nLatches1, &Init1 ); + Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin0) ); + Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin1) ); + Abc_ObjAddFaninL0( pObj->pCopy, nLatches0 ); + Abc_ObjAddFaninL1( pObj->pCopy, nLatches1 ); + // add the initial state + Vec_IntWriteEntry( pNtkNew->vInits, pObj->pCopy->Id, (Init1 << 16) | Init0 ); } - if ( Counter ) - fprintf( stdout, "Latch sweeping removed %d latches (out of %d).\n", Counter, Abc_NtkLatchNum(pNtk) ); - - // redirect fanouts of each latch to the latch fanins - vNodes = Vec_PtrAlloc( 100 ); - Abc_NtkForEachLatch( pNtkNew, pLatch, i ) + // reconnect the POs + Abc_NtkForEachPo( pNtk, pObj, i ) { -//printf( "Latch %s. Fanouts = %d.\n", Abc_ObjName(pLatch), Abc_ObjFanoutNum(pLatch) ); - - Abc_NodeCollectFanouts( pLatch, vNodes ); - Vec_PtrForEachEntry( vNodes, pFanout, k ) - { - if ( Abc_ObjFaninId0(pFanout) == Abc_ObjFaninId1(pFanout)) - printf( " ******* Identical fanins!!! ******* \n" ); - - if ( Abc_ObjFaninId0(pFanout) == (int)pLatch->Id ) - { -// pFaninNew = Abc_ObjNotCond( Abc_ObjChild0(pLatch), Abc_ObjFaninC0(pFanout) ); - pFaninNew = Abc_ObjChild0(pLatch); - Abc_ObjPatchFanin( pFanout, pLatch, pFaninNew ); - Abc_ObjAddFaninL0( pFanout, 1 ); - } - else if ( Abc_ObjFaninId1(pFanout) == (int)pLatch->Id ) - { -// pFaninNew = Abc_ObjNotCond( Abc_ObjChild0(pLatch), Abc_ObjFaninC1(pFanout) ); - pFaninNew = Abc_ObjChild0(pLatch); - Abc_ObjPatchFanin( pFanout, pLatch, pFaninNew ); - Abc_ObjAddFaninL1( pFanout, 1 ); - } - else - assert( 0 ); - } - assert( Abc_ObjFanoutNum(pLatch) == 0 ); - Abc_NtkDeleteObj( pLatch ); + // process the fanins + pFanin0 = Abc_NodeAigToSeq( pObj, 0, &nLatches0, &Init0 ); + Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin0) ); + Abc_ObjAddFaninL0( pObj->pCopy, nLatches0 ); + // add the initial state + Vec_IntWriteEntry( pNtkNew->vInits, pObj->pCopy->Id, Init0 ); } - Vec_PtrFree( vNodes ); - // get rid of latches altogether -// Abc_NtkForEachLatch( pNtkNew, pObj, i ) -// Abc_NtkDeleteObj( pObj ); - assert( pNtkNew->nLatches == 0 ); - Vec_PtrClear( pNtkNew->vLats ); - Vec_PtrShrink( pNtkNew->vCis, pNtk->nPis ); - Vec_PtrShrink( pNtkNew->vCos, pNtk->nPos ); - -/* -///////////////////////////////////////////// -Abc_NtkForEachNode( pNtkNew, pObj, i ) - if ( !Abc_NodeIsConst(pObj) ) - if ( Abc_ObjFaninL0(pObj) + Abc_ObjFaninL1(pObj) > 20 ) - printf( "(%d,%d) ", Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); -Abc_NtkForEachCo( pNtkNew, pObj, i ) - printf( "(%d) ", Abc_ObjFaninL0(pObj) ); -///////////////////////////////////////////// -printf( "\n" ); -*/ - - if ( pNtk->pExdc ) + // set the cutset composed of latch drivers + pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk ); + // copy EXDC and check correctness + if ( pNtkNew->pExdc ) fprintf( stdout, "Warning: EXDC is dropped when converting to sequential AIG.\n" ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkAigToSeq(): Network check has failed.\n" ); @@ -182,282 +132,36 @@ printf( "\n" ); /**Function************************************************************* - Synopsis [Converts a sequential AIG into a logic SOP network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pFanin, * pFaninNew; - int i, k, c; - assert( Abc_NtkIsSeq(pNtk) ); - // start the network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP ); - // create the constant and reset nodes - Abc_NtkDupConst1( pNtk, pNtkNew ); - Abc_NtkDupReset( pNtk, pNtkNew ); - // duplicate the nodes, create node functions and latches - Abc_NtkForEachNode( pNtk, pObj, i ) - { - if ( Abc_NodeIsConst(pObj) ) - continue; - Abc_NtkDupObj(pNtkNew, pObj); - pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); - } - // create latches for the new nodes - Abc_NtkSeqCreateLatches( pNtk, pNtkNew ); - // connect the objects - Abc_NtkForEachObj( pNtk, pObj, i ) - Abc_ObjForEachFanin( pObj, pFanin, k ) - { - // find the fanin - pFaninNew = pFanin->pCopy; - for ( c = 0; c < Abc_ObjFaninL(pObj, k); c++ ) - pFaninNew = pFaninNew->pCopy; - Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); - } - // set the complemented attributed of CO edges (to be fixed by making simple COs) - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( Abc_ObjFaninC0(pObj) ) - Abc_ObjSetFaninC( pObj->pCopy, 0 ); - // fix the problem with complemented and duplicated CO edges - Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); - // duplicate the EXDC network - if ( pNtk->pExdc ) - fprintf( stdout, "Warning: EXDC network is not copied.\n" ); - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkSeqToLogic(): Network check has failed.\n" ); - return pNtkNew; -} - - - - -/**Function************************************************************* - - Synopsis [Finds max number of latches on the fanout edges of each node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkSeqCountLatches( Abc_Ntk_t * pNtk ) -{ - Vec_Int_t * vNumbers; - Abc_Obj_t * pObj; - int i; - assert( Abc_NtkIsSeq( pNtk ) ); - // start the array of counters - vNumbers = Vec_IntAlloc( 0 ); - Vec_IntFill( vNumbers, Abc_NtkObjNumMax(pNtk), 0 ); - // count for each edge - Abc_NtkForEachObj( pNtk, pObj, i ) - Abc_NodeSeqCountLatches( pObj, vNumbers ); - return vNumbers; -} - -/**Function************************************************************* - - Synopsis [Countes the latch numbers due to the fanins edges of the given node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NodeSeqCountLatches( Abc_Obj_t * pObj, Vec_Int_t * vNumbers ) -{ - Abc_Obj_t * pFanin; - int k, nLatches; - // go through each fanin edge - Abc_ObjForEachFanin( pObj, pFanin, k ) - { - nLatches = Abc_ObjFaninL( pObj, k ); - if ( nLatches == 0 ) - continue; - if ( Vec_IntEntry( vNumbers, pFanin->Id ) < nLatches ) - Vec_IntWriteEntry( vNumbers, pFanin->Id, nLatches ); - } -} - - - -/**Function************************************************************* - - Synopsis [Creates latches.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkSeqCreateLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ) -{ - Vec_Int_t * vNumbers; - Abc_Obj_t * pObj; - int i; - assert( Abc_NtkIsSeq( pNtk ) ); - // create latches for each new object according to the counters - vNumbers = Abc_NtkSeqCountLatches( pNtk ); - Abc_NtkForEachObj( pNtk, pObj, i ) - { - if ( pObj->pCopy == NULL ) - continue; - Abc_NodeSeqCreateLatches( pObj->pCopy, Vec_IntEntry(vNumbers, (int)pObj->Id) ); - } - Vec_IntFree( vNumbers ); - // add latch to the PI/PO lists, create latch names - Abc_NtkFinalizeLatches( pNtkNew ); -} - -/**Function************************************************************* - - Synopsis [Creates the given number of latches for this object.] + Synopsis [Collects the cut set nodes.] - Description [The latches are attached to the node and to each other - through the pCopy field.] + Description [These are internal AND gates that fanins into latches.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Abc_NodeSeqCreateLatches( Abc_Obj_t * pObj, int nLatches ) -{ - Abc_Ntk_t * pNtk = pObj->pNtk; - Abc_Obj_t * pLatch, * pFanin; - int i; - pFanin = pObj; - for ( i = 0, pFanin = pObj; i < nLatches; pFanin = pLatch, i++ ) - { - pLatch = Abc_NtkCreateLatch( pNtk ); - Abc_LatchSetInitDc(pLatch); - Abc_ObjAddFanin( pLatch, pFanin ); - pFanin->pCopy = pLatch; - } -} - -/**Function************************************************************* - - Synopsis [Counters the number of latches in the sequential AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk ) -{ - Vec_Int_t * vNumbers; - Abc_Obj_t * pObj; - int i, Counter; - assert( Abc_NtkIsSeq( pNtk ) ); - // create latches for each new object according to the counters - Counter = 0; - vNumbers = Abc_NtkSeqCountLatches( pNtk ); - Abc_NtkForEachPi( pNtk, pObj, i ) - { - assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) ); - Counter += Vec_IntEntry(vNumbers, (int)pObj->Id); - } - Abc_NtkForEachNode( pNtk, pObj, i ) - { - if ( Abc_NodeIsConst(pObj) ) - continue; - assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, (int)pObj->Id) ); - Counter += Vec_IntEntry(vNumbers, (int)pObj->Id); - } - Vec_IntFree( vNumbers ); - if ( Abc_ObjFanoutNum( Abc_AigReset(pNtk->pManFunc) ) > 0 ) - Counter++; - return Counter; -} - - - - - - -/**Function************************************************************* - - Synopsis [Performs forward retiming of the sequential AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk ) +Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk ) { Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode, * pFanout; - int i, k, nLatches; - assert( Abc_NtkIsSeq( pNtk ) ); - // assume that all nodes can be retimed - vNodes = Vec_PtrAlloc( 100 ); - Abc_NtkForEachNode( pNtk, pNode, i ) - { - if ( Abc_NodeIsConst(pNode) ) - continue; - Vec_PtrPush( vNodes, pNode ); - pNode->fMarkA = 1; - } - // process the nodes - Vec_PtrForEachEntry( vNodes, pNode, i ) - { -// printf( "(%d,%d) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) ); - // get the number of latches to retime - nLatches = Abc_ObjFaninLMin(pNode); - if ( nLatches == 0 ) - continue; - assert( nLatches > 0 ); - // subtract these latches on the fanin side - Abc_ObjAddFaninL0( pNode, -nLatches ); - Abc_ObjAddFaninL1( pNode, -nLatches ); - // add these latches on the fanout size - Abc_ObjForEachFanout( pNode, pFanout, k ) - { - Abc_ObjAddFanoutL( pNode, pFanout, nLatches ); - if ( pFanout->fMarkA == 0 ) - { // schedule the node for updating - Vec_PtrPush( vNodes, pFanout ); - pFanout->fMarkA = 1; - } - } - // unmark the node as processed - pNode->fMarkA = 0; - } - Vec_PtrFree( vNodes ); - // clean the marks - Abc_NtkForEachNode( pNtk, pNode, i ) + Abc_Obj_t * pLatch, * pDriver; + int i; + vNodes = Vec_PtrAlloc( Abc_NtkLatchNum(pNtk) ); + Abc_NtkIncrementTravId(pNtk); + Abc_NtkForEachLatch( pNtk, pLatch, i ) { - pNode->fMarkA = 0; - if ( Abc_NodeIsConst(pNode) ) + pDriver = Abc_ObjFanin0(pLatch); + if ( Abc_NodeIsTravIdCurrent(pDriver) || !Abc_NodeIsAigAnd(pDriver) ) continue; - assert( Abc_ObjFaninLMin(pNode) == 0 ); + Abc_NodeSetTravIdCurrent(pDriver); + Vec_PtrPush( vNodes, pDriver->pCopy ); } + return vNodes; } /**Function************************************************************* - Synopsis [Performs forward retiming of the sequential AIG.] + Synopsis [Determines the fanin that is transparent for latches.] Description [] @@ -466,172 +170,28 @@ void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk ) +Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, int * pnInit ) { - Vec_Ptr_t * vNodes; - Abc_Obj_t * pNode, * pFanin, * pFanout; - int i, k, nLatches; - assert( Abc_NtkIsSeq( pNtk ) ); - // assume that all nodes can be retimed - vNodes = Vec_PtrAlloc( 100 ); - Abc_NtkForEachNode( pNtk, pNode, i ) - { - if ( Abc_NodeIsConst(pNode) ) - continue; - Vec_PtrPush( vNodes, pNode ); - pNode->fMarkA = 1; - } - // process the nodes - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - // get the number of latches to retime - nLatches = Abc_ObjFanoutLMin(pNode); - if ( nLatches == 0 ) - continue; - assert( nLatches > 0 ); - // subtract these latches on the fanout side - Abc_ObjForEachFanout( pNode, pFanout, k ) - Abc_ObjAddFanoutL( pNode, pFanout, -nLatches ); - // add these latches on the fanin size - Abc_ObjForEachFanin( pNode, pFanin, k ) - { - Abc_ObjAddFaninL( pNode, k, nLatches ); - if ( Abc_ObjIsPi(pFanin) || Abc_NodeIsConst(pFanin) ) - continue; - if ( pFanin->fMarkA == 0 ) - { // schedule the node for updating - Vec_PtrPush( vNodes, pFanin ); - pFanin->fMarkA = 1; - } - } - // unmark the node as processed - pNode->fMarkA = 0; - } - Vec_PtrFree( vNodes ); - // clean the marks - Abc_NtkForEachNode( pNtk, pNode, i ) + Abc_Obj_t * pFanin; + int Init; + // get the given fanin of the node + pFanin = Abc_ObjFanin( pObj, Num ); + if ( !Abc_ObjIsLatch(pFanin) ) { - pNode->fMarkA = 0; - if ( Abc_NodeIsConst(pNode) ) - continue; -// assert( Abc_ObjFanoutLMin(pNode) == 0 ); + *pnLatches = *pnInit = 0; + return Abc_ObjChild( pObj, Num ); } -} - - - - -/**Function************************************************************* - - Synopsis [Returns the latch number of the fanout.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) -{ - assert( Abc_NtkIsSeq(pObj->pNtk) ); - if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) - return Abc_ObjFaninL0(pFanout); - else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) - return Abc_ObjFaninL1(pFanout); - else - assert( 0 ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Sets the latch number of the fanout.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) -{ - assert( Abc_NtkIsSeq(pObj->pNtk) ); - if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) - Abc_ObjSetFaninL0(pFanout, nLats); - else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) - Abc_ObjSetFaninL1(pFanout, nLats); - else - assert( 0 ); -} - -/**Function************************************************************* - - Synopsis [Adds to the latch number of the fanout.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) -{ - assert( Abc_NtkIsSeq(pObj->pNtk) ); - if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) - Abc_ObjAddFaninL0(pFanout, nLats); - else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) - Abc_ObjAddFaninL1(pFanout, nLats); - else - assert( 0 ); -} - -/**Function************************************************************* - - Synopsis [Returns the latch number of the fanout.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ObjFanoutLMax( Abc_Obj_t * pObj ) -{ - Abc_Obj_t * pFanout; - int i, nLatch, nLatchRes; - nLatchRes = 0; - Abc_ObjForEachFanout( pObj, pFanout, i ) - if ( nLatchRes < (nLatch = Abc_ObjFanoutL(pObj, pFanout)) ) - nLatchRes = nLatch; - assert( nLatchRes >= 0 ); - return nLatchRes; -} - -/**Function************************************************************* - - Synopsis [Returns the latch number of the fanout.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ObjFanoutLMin( Abc_Obj_t * pObj ) -{ - Abc_Obj_t * pFanout; - int i, nLatch, nLatchRes; - nLatchRes = ABC_INFINITY; - Abc_ObjForEachFanout( pObj, pFanout, i ) - if ( nLatchRes > (nLatch = Abc_ObjFanoutL(pObj, pFanout)) ) - nLatchRes = nLatch; - assert( nLatchRes < ABC_INFINITY ); - return nLatchRes; + pFanin = Abc_NodeAigToSeq( pFanin, 0, pnLatches, pnInit ); + // get the new initial state + Init = Abc_LatchInit(pObj); + assert( Init >= 0 && Init <= 3 ); + // complement the initial state if the inv is retimed over the latch + if ( Abc_ObjIsComplement(pFanin) && Init < 2 ) // not a don't-care + Init ^= 3; + // update the latch number and initial state + (*pnLatches)++; + (*pnInit) = ((*pnInit) << 2) | Init; + return Abc_ObjNotCond( pFanin, Abc_ObjFaninC(pObj,Num) ); } diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c new file mode 100644 index 00000000..8dccb81d --- /dev/null +++ b/src/base/abcs/abcUtils.c @@ -0,0 +1,243 @@ +/**CFile**************************************************************** + + FileName [abcUtils.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Utilities working sequential AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcUtils.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the latch number of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout ) +{ + assert( Abc_NtkIsSeq(pObj->pNtk) ); + if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) + return Abc_ObjFaninL0(pFanout); + else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) + return Abc_ObjFaninL1(pFanout); + else + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Sets the latch number of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) +{ + assert( Abc_NtkIsSeq(pObj->pNtk) ); + if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) + Abc_ObjSetFaninL0(pFanout, nLats); + else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) + Abc_ObjSetFaninL1(pFanout, nLats); + else + assert( 0 ); +} + +/**Function************************************************************* + + Synopsis [Adds to the latch number of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats ) +{ + assert( Abc_NtkIsSeq(pObj->pNtk) ); + if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id ) + Abc_ObjAddFaninL0(pFanout, nLats); + else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id ) + Abc_ObjAddFaninL1(pFanout, nLats); + else + assert( 0 ); +} + +/**Function************************************************************* + + Synopsis [Returns the latch number of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjFanoutLMax( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanout; + int i, nLatchCur, nLatchRes; + nLatchRes = 0; + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + nLatchCur = Abc_ObjFanoutL(pObj, pFanout); + if ( nLatchRes < nLatchCur ) + nLatchRes = nLatchCur; + } + assert( nLatchRes >= 0 ); + return nLatchRes; +} + +/**Function************************************************************* + + Synopsis [Returns the latch number of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjFanoutLMin( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanout; + int i, nLatchCur, nLatchRes; + nLatchRes = ABC_INFINITY; + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + nLatchCur = Abc_ObjFanoutL(pObj, pFanout); + if ( nLatchRes > nLatchCur ) + nLatchRes = nLatchCur; + } + assert( nLatchRes < ABC_INFINITY ); + return nLatchRes; +} + +/**Function************************************************************* + + Synopsis [Returns the sum of latches on the fanout edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjFanoutLSum( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanout; + int i, nSum = 0; + Abc_ObjForEachFanout( pObj, pFanout, i ) + nSum += Abc_ObjFanoutL(pObj, pFanout); + return nSum; +} + +/**Function************************************************************* + + Synopsis [Returns the sum of latches on the fanin edges.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjFaninLSum( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanin; + int i, nSum = 0; + Abc_ObjForEachFanin( pObj, pFanin, i ) + nSum += Abc_ObjFaninL(pObj, i); + return nSum; +} + +/**Function************************************************************* + + Synopsis [Counters the number of latches in the sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i, Counter; + assert( Abc_NtkIsSeq( pNtk ) ); + Counter = 0; + Abc_NtkForEachNode( pNtk, pObj, i ) + Counter += Abc_ObjFaninLSum( pObj ); + Abc_NtkForEachPo( pNtk, pObj, i ) + Counter += Abc_ObjFaninLSum( pObj ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Counters the number of latches in the sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i, Counter; + assert( Abc_NtkIsSeq( pNtk ) ); + Counter = 0; + Abc_NtkForEachPi( pNtk, pObj, i ) + Counter += Abc_ObjFanoutLMax( pObj ); + Abc_NtkForEachNode( pNtk, pObj, i ) + Counter += Abc_ObjFanoutLMax( pObj ); + return Counter; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |