summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2005-09-12 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2005-09-12 08:01:00 -0700
commitc065b2c5daea65cb98659aa1bb56a138ca7cc290 (patch)
tree8a13866910599fe7fe347fa4fbefe8bfd5693550
parent798bbfc5a9b6f7dd5b47425c8c7026762451b0ba (diff)
downloadabc-c065b2c5daea65cb98659aa1bb56a138ca7cc290.tar.gz
abc-c065b2c5daea65cb98659aa1bb56a138ca7cc290.tar.bz2
abc-c065b2c5daea65cb98659aa1bb56a138ca7cc290.zip
Version abc50912
-rw-r--r--abc.dsp18
-rw-r--r--abc.optbin51712 -> 51712 bytes
-rw-r--r--abc.plg56
-rw-r--r--src/base/abc/abc.h49
-rw-r--r--src/base/abc/abcAig.c24
-rw-r--r--src/base/abc/abcCheck.c2
-rw-r--r--src/base/abc/abcNames.c18
-rw-r--r--src/base/abc/abcNetlist.c1
-rw-r--r--src/base/abc/abcNtk.c1
-rw-r--r--src/base/abc/abcObj.c29
-rw-r--r--src/base/abc/abcUtil.c4
-rw-r--r--src/base/abci/abc.c17
-rw-r--r--src/base/abci/abcFraig.c5
-rw-r--r--src/base/abci/abcPrint.c1
-rw-r--r--src/base/abcs/abcForBack.c161
-rw-r--r--src/base/abcs/abcLogic.c140
-rw-r--r--src/base/abcs/abcRetCore.c145
-rw-r--r--src/base/abcs/abcRetDelay.c (renamed from src/base/abcs/abcRetime.c)14
-rw-r--r--src/base/abcs/abcRetImpl.c362
-rw-r--r--src/base/abcs/abcRetUtil.c227
-rw-r--r--src/base/abcs/abcSeq.c212
-rw-r--r--src/base/abcs/abcShare.c154
-rw-r--r--src/base/abcs/abcUtils.c165
-rw-r--r--src/base/abcs/abcs.h315
-rw-r--r--src/base/io/ioReadBench.c5
-rw-r--r--src/base/io/ioReadBlif.c10
-rw-r--r--src/base/io/ioReadEdif.c3
-rw-r--r--src/base/io/ioUtil.c2
-rw-r--r--src/base/io/ioWriteBlif.c2
-rw-r--r--src/sat/csat/csat_apis.c2
30 files changed, 1518 insertions, 626 deletions
diff --git a/abc.dsp b/abc.dsp
index 3fa16b14..237445da 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -270,15 +270,23 @@ SOURCE=.\src\base\abci\abcVerify.c
# PROP Default_Filter ""
# Begin Source File
-SOURCE=.\src\base\abcs\abcForBack.c
+SOURCE=.\src\base\abcs\abcRetCore.c
# End Source File
# Begin Source File
-SOURCE=.\src\base\abcs\abcLogic.c
+SOURCE=.\src\base\abcs\abcRetDelay.c
# End Source File
# Begin Source File
-SOURCE=.\src\base\abcs\abcRetime.c
+SOURCE=.\src\base\abcs\abcRetImpl.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abcs\abcRetUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\abcs\abcs.h
# End Source File
# Begin Source File
@@ -286,6 +294,10 @@ SOURCE=.\src\base\abcs\abcSeq.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\abcs\abcShare.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\abcs\abcUtils.c
# End Source File
# End Group
diff --git a/abc.opt b/abc.opt
index f0f7bca1..0e644e73 100644
--- a/abc.opt
+++ b/abc.opt
Binary files differ
diff --git a/abc.plg b/abc.plg
index 5e439a6b..75756b18 100644
--- a/abc.plg
+++ b/abc.plg
@@ -6,13 +6,23 @@
--------------------Configuration: abc - Win32 Debug--------------------
</h3>
<h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1AD8.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1CE4.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\base\abcs\abcLogic.c"
+"C:\_projects\abc\src\base\abc\abcNetlist.c"
+"C:\_projects\abc\src\base\abc\abcUtil.c"
+"C:\_projects\abc\src\base\abci\abc.c"
+"C:\_projects\abc\src\base\abci\abcPrint.c"
+"C:\_projects\abc\src\base\abcs\abcSeq.c"
+"C:\_projects\abc\src\base\abcs\abcUtils.c"
+"C:\_projects\abc\src\base\abcs\abcShare.c"
+"C:\_projects\abc\src\base\abcs\abcRetDelay.c"
+"C:\_projects\abc\src\base\abcs\abcRetImpl.c"
+"C:\_projects\abc\src\base\abcs\abcRetUtil.c"
+"C:\_projects\abc\src\base\abcs\abcRetCore.c"
]
-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
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1CE4.tmp"
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1CE5.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
@@ -55,8 +65,8 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\abcTiming.obj
.\Debug\abcUnreach.obj
.\Debug\abcVerify.obj
-.\Debug\abcRetime.obj
.\Debug\abcSeq.obj
+.\Debug\abcUtils.obj
.\Debug\cmd.obj
.\Debug\cmdAlias.obj
.\Debug\cmdApi.obj
@@ -310,16 +320,28 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\mvcPrint.obj
.\Debug\mvcSort.obj
.\Debug\mvcUtils.obj
-.\Debug\abcLogic.obj
-.\Debug\abcUtils.obj
-.\Debug\abcForBack.obj
+.\Debug\abcShare.obj
+.\Debug\abcRetDelay.obj
+.\Debug\abcRetImpl.obj
+.\Debug\abcRetUtil.obj
+.\Debug\abcRetCore.obj
]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1AD9.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1CE5.tmp"
<h3>Output Window</h3>
Compiling...
-abcLogic.c
+abcNetlist.c
+abcUtil.c
+abc.c
+abcPrint.c
+abcSeq.c
+abcUtils.c
+abcShare.c
+abcRetDelay.c
+abcRetImpl.c
+abcRetUtil.c
+abcRetCore.c
Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1ADA.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1CE6.tmp" with contents
[
/nologo /o"Debug/abc.bsc"
.\Debug\abcAig.sbr
@@ -362,8 +384,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1ADA.tmp" with cont
.\Debug\abcTiming.sbr
.\Debug\abcUnreach.sbr
.\Debug\abcVerify.sbr
-.\Debug\abcRetime.sbr
.\Debug\abcSeq.sbr
+.\Debug\abcUtils.sbr
.\Debug\cmd.sbr
.\Debug\cmdAlias.sbr
.\Debug\cmdApi.sbr
@@ -617,10 +639,12 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1ADA.tmp" with cont
.\Debug\mvcPrint.sbr
.\Debug\mvcSort.sbr
.\Debug\mvcUtils.sbr
-.\Debug\abcLogic.sbr
-.\Debug\abcUtils.sbr
-.\Debug\abcForBack.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1ADA.tmp"
+.\Debug\abcShare.sbr
+.\Debug\abcRetDelay.sbr
+.\Debug\abcRetImpl.sbr
+.\Debug\abcRetUtil.sbr
+.\Debug\abcRetCore.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1CE6.tmp"
Creating browse info file...
<h3>Output Window</h3>
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 02b284e6..49dd9943 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -43,7 +43,7 @@
// network types
typedef enum {
- ABC_TYPE_NONE, // 0: unknown
+ ABC_TYPE_NONE = 0, // 0: unknown
ABC_TYPE_NETLIST, // 1: network with PIs/POs, latches, nodes, and nets
ABC_TYPE_LOGIC, // 2: network with PIs/POs, latches, and nodes
ABC_TYPE_STRASH, // 3: structurally hashed AIG (two input AND gates with c-attributes on edges)
@@ -53,7 +53,7 @@ typedef enum {
// network functionality
typedef enum {
- ABC_FUNC_NONE, // 0: unknown
+ ABC_FUNC_NONE = 0, // 0: unknown
ABC_FUNC_SOP, // 1: sum-of-products
ABC_FUNC_BDD, // 2: binary decision diagrams
ABC_FUNC_AIG, // 3: and-inverter graphs
@@ -76,7 +76,7 @@ typedef enum {
// object types
typedef enum {
- ABC_OBJ_NONE, // 0: unknown
+ ABC_OBJ_NONE = 0, // 0: unknown
ABC_OBJ_NET, // 1: net
ABC_OBJ_NODE, // 2: node
ABC_OBJ_LATCH, // 3: latch
@@ -85,6 +85,14 @@ typedef enum {
ABC_OBJ_OTHER // 6: unused
} Abc_ObjType_t;
+// latch initial values
+typedef enum {
+ ABC_INIT_NONE = 0, // 0: unknown
+ ABC_INIT_ZERO, // 1: zero
+ ABC_INIT_ONE, // 2: one
+ ABC_INIT_DC // 3: don't-care
+} Abc_InitType_t;
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
@@ -317,13 +325,6 @@ static inline void Abc_ObjSetFaninL1( Abc_Obj_t * pObj, int nLats )
static inline void Abc_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats ) { pObj->vFanins.pArray[i].nLats += nLats; }
static inline void Abc_ObjAddFaninL0( Abc_Obj_t * pObj, int nLats ) { pObj->vFanins.pArray[0].nLats += nLats; }
static inline void Abc_ObjAddFaninL1( Abc_Obj_t * pObj, int nLats ) { pObj->vFanins.pArray[1].nLats += nLats; }
-extern int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout );
-extern void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats );
-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; }
@@ -342,12 +343,12 @@ 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 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 void Abc_LatchSetInit0( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ZERO; }
+static inline void Abc_LatchSetInit1( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE; }
+static inline void Abc_LatchSetInitDc( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC; }
+static inline bool Abc_LatchIsInit0( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
+static inline bool Abc_LatchIsInit1( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE; }
+static inline bool Abc_LatchIsInitDc( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC; }
static inline int Abc_LatchInit( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); return (int)pLatch->pData; }
// outputs the runtime in seconds
@@ -409,7 +410,6 @@ extern int Abc_AigCleanup( Abc_Aig_t * pMan );
extern bool Abc_AigCheck( Abc_Aig_t * pMan );
extern int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan );
-extern Abc_Obj_t * Abc_AigReset( Abc_Aig_t * pMan );
extern Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
@@ -515,6 +515,7 @@ extern char * Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pNam
extern char * Abc_ObjName( Abc_Obj_t * pNode );
extern char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
extern char * Abc_ObjNameUnique( Abc_Ntk_t * pNtk, char * pName );
+extern char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
extern char * Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pNameOld );
extern char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix );
extern void Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk );
@@ -585,20 +586,6 @@ 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 );
-
-/*=== 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/abcAig.c b/src/base/abc/abcAig.c
index 701fb90f..e1361eb7 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -49,7 +49,7 @@ struct Abc_Aig_t_
{
Abc_Ntk_t * pNtkAig; // the AIG network
Abc_Obj_t * pConst1; // the constant 1 node
- Abc_Obj_t * pReset; // the sequential reset node
+// Abc_Obj_t * pReset; // the sequential reset node
Abc_Obj_t ** pBins; // the table bins
int nBins; // the size of the table
int nEntries; // the total number of entries in the table
@@ -125,9 +125,8 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
pMan->pNtkAig = pNtkAig;
// allocate constant nodes
pMan->pConst1 = Abc_NtkCreateNode( pNtkAig );
- pMan->pReset = Abc_NtkCreateNode( pNtkAig );
// subtract these nodes from the total number
- pNtkAig->nNodes -= 2;
+ pNtkAig->nNodes -= 1;
return pMan;
}
@@ -153,7 +152,6 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
assert( Abc_NtkLatchNum(pMan->pNtkAig) == Abc_NtkLatchNum(pManNew->pNtkAig) );
// set mapping of the constant nodes
Abc_AigConst1( pMan )->pCopy = Abc_AigConst1( pManNew );
- Abc_AigReset( pMan )->pCopy = Abc_AigReset( pManNew );
// set the mapping of CIs/COs
Abc_NtkForEachPi( pMan->pNtkAig, pObj, i )
pObj->pCopy = Abc_NtkPi( pManNew->pNtkAig, i );
@@ -264,7 +262,7 @@ bool Abc_AigCheck( Abc_Aig_t * pMan )
nFanins = Abc_ObjFaninNum(pObj);
if ( nFanins == 0 )
{
- if ( pObj != pMan->pConst1 && pObj != pMan->pReset )
+ if ( pObj != pMan->pConst1 )
{
printf( "Abc_AigCheck: The AIG has non-standard constant nodes.\n" );
return 0;
@@ -340,22 +338,6 @@ Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan )
return pMan->pConst1;
}
-/**Function*************************************************************
-
- Synopsis [Read the reset node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_AigReset( Abc_Aig_t * pMan )
-{
- return pMan->pReset;
-}
-
/**Function*************************************************************
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index b91a1291..773096a0 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -565,7 +565,7 @@ bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
Value = 0;
}
// make sure the latch has a reasonable return value
- if ( (int)pLatch->pData < 0 || (int)pLatch->pData > 2 )
+ if ( (int)pLatch->pData < ABC_INIT_ZERO || (int)pLatch->pData > ABC_INIT_DC )
{
fprintf( stdout, "NodeCheck: Latch \"%s\" has incorrect reset value (%d).\n",
Abc_ObjName(pLatch), (int)pLatch->pData );
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index 2bf6461b..53ac6e07 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -162,6 +162,24 @@ char * Abc_ObjNameUnique( Abc_Ntk_t * pNtk, char * pName )
return NULL;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the dummy PI name.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
+{
+ static char Buffer[100];
+ sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num );
+ return Buffer;
+}
+
/**Function*************************************************************
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 08ee93bb..4cda189d 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abc.h"
+#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index dc4dd9e2..e543bf19 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -504,6 +504,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
Vec_PtrFree( pNtk->vPtrTemp );
Vec_IntFree( pNtk->vIntTemp );
Vec_StrFree( pNtk->vStrTemp );
+ if ( pNtk->vInits ) Vec_IntFree( pNtk->vInits );
// free the hash table of Obj name into Obj ID
stmm_free_table( pNtk->tName2Net );
stmm_free_table( pNtk->tObj2Name );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index eddfd8b8..15753f4e 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -196,34 +196,6 @@ Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
/**Function*************************************************************
- Synopsis [Creates a new constant node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
-{
- Abc_Obj_t * pReset, * pConst1;
- assert( Abc_NtkHasAig(pNtkAig) );
- assert( Abc_NtkIsLogic(pNtkNew) );
- pReset = Abc_AigReset(pNtkAig->pManFunc);
- if ( Abc_ObjFanoutNum(pReset) > 0 )
- {
- // create new latch with reset value 0
- pReset->pCopy = Abc_NtkCreateLatch( pNtkNew );
- // add constant node fanin to the latch
- pConst1 = Abc_NodeCreateConst1( pNtkNew );
- Abc_ObjAddFanin( pReset->pCopy, pConst1 );
- }
- return pReset->pCopy;
-}
-
-/**Function*************************************************************
-
Synopsis [Deletes the object from the network.]
Description []
@@ -493,6 +465,7 @@ Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_LATCH );
+ pObj->pData = (void *)ABC_INIT_NONE;
Abc_ObjAdd( pObj );
return pObj;
}
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 0f7a4ab8..bc71143b 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -22,6 +22,7 @@
#include "main.h"
#include "mio.h"
#include "dec.h"
+#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -931,9 +932,6 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
pConst1 = Abc_AigConst1(pNtk->pManFunc);
pConst1->Id = Vec_PtrSize( vObjsNew );
Vec_PtrPush( vObjsNew, pConst1 );
- pReset = Abc_AigReset(pNtk->pManFunc);
- pReset->Id = Vec_PtrSize( vObjsNew );
- Vec_PtrPush( vObjsNew, pReset );
}
// put PI nodes next
Abc_NtkForEachPi( pNtk, pNode, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f2cfaaf1..4745273e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25,6 +25,7 @@
#include "fpga.h"
#include "pga.h"
#include "cut.h"
+#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -3981,6 +3982,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fForward;
int fBackward;
+ int fInitial;
extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
@@ -3989,10 +3991,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fForward = 0;
+ fForward = 0;
fBackward = 0;
+ fInitial = 0;
util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "fbh" ) ) != EOF )
+ while ( ( c = util_getopt( argc, argv, "fbih" ) ) != EOF )
{
switch ( c )
{
@@ -4002,6 +4005,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b':
fBackward ^= 1;
break;
+ case 'i':
+ fInitial ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -4030,15 +4036,18 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkSeqRetimeForward( pNtk );
else if ( fBackward )
Abc_NtkSeqRetimeBackward( pNtk );
+ else if ( fInitial )
+ Abc_NtkSeqRetimeInitial( pNtk );
else
Abc_NtkSeqRetimeDelay( pNtk );
return 0;
usage:
- fprintf( pErr, "usage: retime [-fbh]\n" );
- fprintf( pErr, "\t retimes sequential AIG (default is Pan's algorithm)\n" );
+ fprintf( pErr, "usage: retime [-fbih]\n" );
+ fprintf( pErr, "\t retimes sequential AIG (default is Pan's delay-optimal retiming)\n" );
fprintf( pErr, "\t-f : toggle forward retiming [default = %s]\n", fForward? "yes": "no" );
fprintf( pErr, "\t-b : toggle backward retiming [default = %s]\n", fBackward? "yes": "no" );
+ fprintf( pErr, "\t-i : toggle retiming for initial state [default = %s]\n", fInitial? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 7a8eed5d..fe4f0511 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -88,7 +88,7 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
ProgressBar * pProgress;
Fraig_Node_t * pNodeFraig;
Vec_Ptr_t * vNodes;
- Abc_Obj_t * pNode, * pConst1, * pReset;
+ Abc_Obj_t * pNode, * pConst1;
int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
int i;
@@ -102,7 +102,6 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
pConst1 = Abc_AigConst1( pNtk->pManFunc );
- pReset = Abc_AigReset( pNtk->pManFunc );
// perform strashing
vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -114,8 +113,6 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pNode == pConst1 )
pNodeFraig = Fraig_ManReadConst1(pMan);
- else if ( pNode == pReset )
- continue;
else
pNodeFraig = Fraig_NodeAnd( pMan,
Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e4af8e12..26ce3665 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -20,6 +20,7 @@
#include "abc.h"
#include "dec.h"
+#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/abcs/abcForBack.c b/src/base/abcs/abcForBack.c
deleted file mode 100644
index 4db162e1..00000000
--- a/src/base/abcs/abcForBack.c
+++ /dev/null
@@ -1,161 +0,0 @@
-/**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
deleted file mode 100644
index f33ed40e..00000000
--- a/src/base/abcs/abcLogic.c
+++ /dev/null
@@ -1,140 +0,0 @@
-/**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/abcRetCore.c b/src/base/abcs/abcRetCore.c
new file mode 100644
index 00000000..f6ba0c59
--- /dev/null
+++ b/src/base/abcs/abcRetCore.c
@@ -0,0 +1,145 @@
+/**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 "abcs.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 Abc_RetStep_t_)
+ - as a set of node moves, fwd and bwd (two arrays arrays of Abc_Obj_t *)
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs most forward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vMoves;
+ Abc_Obj_t * pNode;
+ int i;
+ // 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
+ Abc_NtkImplementRetimingForward( pNtk, vMoves );
+ Vec_PtrFree( vMoves );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs most backward retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vMoves;
+ Abc_Obj_t * pNode;
+ int i, RetValue;
+ // 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 = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
+ Vec_PtrFree( vMoves );
+ if ( RetValue == 0 )
+ printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs performs optimal delay retiming.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
+{
+ Vec_Str_t * vLags;
+ int RetValue;
+ // get the retiming vector
+ vLags = Abc_NtkSeqRetimeDelayLags( pNtk );
+ // implement this retiming
+ RetValue = Abc_NtkImplementRetiming( pNtk, vLags );
+ Vec_StrFree( vLags );
+ if ( RetValue == 0 )
+ printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs retiming for initial state computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk )
+{
+ Vec_Str_t * vLags;
+ int RetValue;
+ // get the retiming vector
+ vLags = Abc_NtkSeqRetimeDelayLags( pNtk );
+ // implement this retiming
+ RetValue = Abc_NtkImplementRetiming( pNtk, vLags );
+ Vec_StrFree( vLags );
+ if ( RetValue == 0 )
+ printf( "Retiming completed but initial state computation has failed.\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcRetime.c b/src/base/abcs/abcRetDelay.c
index 13b8a926..71114171 100644
--- a/src/base/abcs/abcRetime.c
+++ b/src/base/abcs/abcRetDelay.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "abc.h"
+#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -51,9 +51,11 @@ enum { ABC_UPDATE_FAIL, ABC_UPDATE_NO, ABC_UPDATE_YES };
SeeAlso []
***********************************************************************/
-void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
+Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk )
{
- int FiMax, FiBest;
+ Vec_Str_t * vLags;
+ Abc_Obj_t * pNode;
+ int i, FiMax, FiBest;
assert( Abc_NtkIsSeq( pNtk ) );
// start storage for sequential arrival times
@@ -71,9 +73,15 @@ void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
// print the result
printf( "The best clock period is %3d.\n", FiBest );
+ // convert to lags
+ vLags = Vec_StrStart( Abc_NtkObjNumMax(pNtk) );
+ Abc_AigForEachAnd( pNtk, pNode, i )
+ Vec_StrWriteEntry( vLags, i, (char)(Abc_NodeReadLValue(pNode) / FiBest) );
+
// free storage
Vec_IntFree( pNtk->pData );
pNtk->pData = NULL;
+ return vLags;
}
/**Function*************************************************************
diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c
new file mode 100644
index 00000000..9a28a354
--- /dev/null
+++ b/src/base/abcs/abcRetImpl.c
@@ -0,0 +1,362 @@
+/**CFile****************************************************************
+
+ FileName [abcRetImpl.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Implementation of retiming.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcRetImpl.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+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 );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Implements the retiming on the sequential AIG.]
+
+ Description [Split the retiming into forward and backward.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags )
+{
+ Vec_Int_t * vSteps;
+ Vec_Ptr_t * vMoves;
+ int RetValue;
+
+ // forward retiming
+ vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 );
+ // translate each set of steps into moves
+ vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 );
+ // implement this retiming
+ Abc_NtkImplementRetimingForward( pNtk, vMoves );
+ Vec_IntFree( vSteps );
+ Vec_PtrFree( vMoves );
+
+ // backward retiming
+ vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 );
+ // translate each set of steps into moves
+ vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 );
+ // implement this retiming
+ RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves );
+ Vec_IntFree( vSteps );
+ Vec_PtrFree( vMoves );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the given retiming on the sequential AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_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 [Implements the given retiming on the sequential AIG.]
+
+ Description [Returns 0 of initial state computation fails.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves )
+{
+ Abc_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, Init, nDigits, RetValue, i;
+
+ // return if the retiming is trivial
+ if ( Vec_PtrSize(vMoves) == 0 )
+ return 1;
+
+ // start the table and the array of PO values
+ tTable = stmm_init_table( stmm_numcmp, stmm_numhash );
+ vValues = Vec_IntAlloc( 100 );
+
+ // create the network for the initial state computation
+ pNtkProb = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP );
+
+ // perform the backward moves and build the network
+ Vec_PtrForEachEntry( vMoves, pNode, i )
+ 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
+ nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtkProb) );
+ Abc_NtkForEachPi( pNtkProb, pNodeNew, i )
+ Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("pi", i, nDigits) );
+ nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtkProb) );
+ Abc_NtkForEachPo( pNtkProb, pNodeNew, i )
+ Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("po", i, nDigits) );
+
+ // make sure everything is okay with the network structure
+ if ( !Abc_NtkDoCheck( pNtkProb ) )
+ {
+ printf( "Abc_NtkImplementRetimingBackward: The internal network check has failed.\n" );
+ return 0;
+ }
+
+ // get the miter cone
+ pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues );
+ Abc_NtkDelete( pNtkProb );
+ Vec_IntFree( vValues );
+
+ // 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
+ RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 );
+ pModel = pNtkCnf->pModel; pNtkCnf->pModel = NULL;
+ Abc_NtkDelete( pNtkCnf );
+
+ // analyze the result
+ if ( RetValue == -1 || RetValue == 1 )
+ {
+ stmm_free_table( tTable );
+ return 0;
+ }
+
+ // set the values of the latches
+ i = 0;
+ stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew )
+ {
+ pNode = Abc_NtkObj( pNtk, RetEdge.iNode );
+ Init = pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO;
+ Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init );
+ i++;
+ }
+ stmm_free_table( tTable );
+ free( pModel );
+ return 1;
+}
+
+/**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( Abc_ObjFaninL0(pObj) >= 1 );
+ assert( Abc_ObjFaninL1(pObj) >= 1 );
+ // remove the init values from the fanins
+ Init0 = Abc_ObjFaninLDeleteFirst( pObj, 0 );
+ Init1 = Abc_ObjFaninLDeleteFirst( 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;
+ // add the init values to the fanouts
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pFanout, pObj), Init );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Retimes node backward by one latch.]
+
+ Description [Constructs the problem for initial state computation.]
+
+ 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;
+ Abc_RetEdge_t Edge;
+ Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuf;
+ unsigned Entry;
+ int i, fMet0, fMet1, fMetX;
+
+ // make sure the node can be retimed
+ assert( Abc_ObjFanoutLMin(pObj) > 0 );
+ // get the fanout values
+ fMet0 = fMet1 = fMetX = 0;
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ {
+ Init = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) );
+ if ( Init == ABC_INIT_ZERO )
+ fMet0 = 1;
+ else if ( Init == ABC_INIT_ONE )
+ fMet1 = 1;
+ else if ( Init == ABC_INIT_NONE )
+ fMetX = 1;
+ }
+ // quit if conflict is found
+ if ( fMet0 && fMet1 )
+ return 0;
+
+ // get the new initial value
+ if ( !fMet0 && !fMet1 && !fMetX )
+ {
+ Init = ABC_INIT_DC;
+ // do not add the node
+ pNodeNew = NULL;
+ }
+ else
+ {
+ Init = ABC_INIT_NONE;
+ // add the node to the network
+ pNodeNew = Abc_NtkCreateNode( pNtkNew );
+ pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ }
+
+ // perform the changes
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ {
+ Edge.iNode = pFanout->Id;
+ Edge.iEdge = Abc_ObjEdgeNum(pObj, pFanout);
+ Edge.iLatch = Abc_ObjFaninL( pFanout, Edge.iEdge ) - 1;
+ // try to delete this edge
+ stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew );
+ // delete the entry
+ Value = Abc_ObjFaninLDeleteLast( pFanout, Edge.iEdge );
+ if ( Value == ABC_INIT_NONE )
+ Abc_ObjAddFanin( pFanoutNew, pNodeNew );
+ }
+
+ // update the table for each of the edges
+ Abc_ObjFaninLForEachValue( pObj, 0, Entry, i, Value )
+ {
+ if ( Value != ABC_INIT_NONE )
+ continue;
+ if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
+ assert( 0 );
+ Edge.iLatch++;
+ if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
+ assert( 0 );
+ }
+ Abc_ObjFaninLForEachValue( pObj, 1, Entry, i, Value )
+ {
+ if ( Value != ABC_INIT_NONE )
+ continue;
+ if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) )
+ assert( 0 );
+ Edge.iLatch++;
+ if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) )
+ assert( 0 );
+ }
+ Abc_ObjFaninLInsertFirst( pObj, 0, Init );
+ Abc_ObjFaninLInsertFirst( pObj, 1, Init );
+
+ // do not insert the don't-care node into the network
+ if ( Init == ABC_INIT_DC )
+ return 1;
+
+ // add the buffer
+ pBuf = Abc_NtkCreateNode( pNtkNew );
+ pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+ Abc_ObjAddFanin( pNodeNew, pBuf );
+ // point to it from the table
+ Edge.iNode = pObj->Id;
+ Edge.iEdge = 0;
+ Edge.iLatch = 0;
+ if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+ assert( 0 );
+
+ // add the buffer
+ pBuf = Abc_NtkCreateNode( pNtkNew );
+ pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+ Abc_ObjAddFanin( pNodeNew, pBuf );
+ // point to it from the table
+ Edge.iNode = pObj->Id;
+ Edge.iEdge = 1;
+ Edge.iLatch = 0;
+ if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) )
+ assert( 0 );
+
+ // check if the output value is required
+ if ( fMet0 || fMet1 )
+ {
+ // add the PO and the value
+ Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
+ Vec_IntPush( vValues, fMet1 );
+ }
+ return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcRetUtil.c b/src/base/abcs/abcRetUtil.c
new file mode 100644
index 00000000..52ea6446
--- /dev/null
+++ b/src/base/abcs/abcRetUtil.c
@@ -0,0 +1,227 @@
+/**CFile****************************************************************
+
+ FileName [abcRetUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Retiming utilities.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcRetUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**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) ", Abc_ObjFaninL0(pNode), Abc_ObjFaninL0(pNode) );
+ // unmark the node as processed
+ pNode->fMarkA = 0;
+ // get the number of latches to retime
+ if ( fForward )
+ nLatches = Abc_ObjFaninLMin(pNode);
+ else
+ nLatches = Abc_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( Abc_ObjFaninLMin(pNode) == 0 );
+ else
+ assert( Abc_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 )
+{
+ Abc_RetStep_t RetStep;
+ Vec_Ptr_t * vMoves;
+ Abc_Obj_t * pNode;
+ int i, k, iNode, nLatches, Number;
+ assert( Abc_NtkIsSeq( pNtk ) );
+ // process the nodes
+ vMoves = Vec_PtrAlloc( 100 );
+ while ( Vec_IntSize(vSteps) > 0 )
+ {
+ iNode = 0;
+ Vec_IntForEachEntry( vSteps, Number, i )
+ {
+ // get the retiming step
+ RetStep = Abc_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 = Abc_ObjFaninLMin(pNode);
+ else
+ nLatches = Abc_ObjFanoutLMin(pNode);
+ if ( nLatches == 0 )
+ {
+ Vec_IntWriteEntry( vSteps, iNode++, Abc_RetStep2Int(RetStep) );
+ continue;
+ }
+ assert( nLatches > 0 );
+ // 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++, Abc_RetStep2Int(RetStep) );
+ }
+ // reduce the array
+ Vec_IntShrink( vSteps, iNode );
+ }
+ // 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;
+ Abc_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, Abc_RetStep2Int(RetStep) );
+ }
+ else if ( Value > 0 && !fForward )
+ {
+ RetStep.iNode = i;
+ RetStep.nLatches = Value;
+ Vec_IntPush( vNodes, Abc_RetStep2Int(RetStep) );
+ }
+ }
+ return vNodes;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c
index eca337fd..1264a98d 100644
--- a/src/base/abcs/abcSeq.c
+++ b/src/base/abcs/abcSeq.c
@@ -18,20 +18,23 @@
***********************************************************************/
-#include "abc.h"
+#include "abcs.h"
/*
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.
+
+ When converting AIG into sequential AIG:
+ - 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
@@ -46,7 +49,8 @@
////////////////////////////////////////////////////////////////////////
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 );
+static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pAnd, int Num, int * pnLatches, unsigned * pnInit );
+static Abc_Obj_t * Abc_NodeSeqToLogic( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pFanin, int nLatches, unsigned Init );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@@ -54,11 +58,11 @@ static Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pAnd, int Num, int * pnLatches,
/**Function*************************************************************
- Synopsis [Converts a normal AIG into a sequential AIG.]
+ Synopsis [Converts combinational AIG with latches into sequential AIG.]
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.]
+ are not duplicated. The choice nodes are duplicated.]
SideEffects []
@@ -69,8 +73,8 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Vec_Ptr_t * vNodes;
- Abc_Obj_t * pObj, * pFanin0, * pFanin1;
- int i, nLatches0, nLatches1, Init0, Init1;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, Init, nLatches;
// make sure it is an AIG without self-feeding latches
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
@@ -93,32 +97,35 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
// copy the internal nodes, including choices, excluding dangling
vNodes = Abc_AigDfs( pNtk, 0, 0 );
Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
Abc_NtkDupObj(pNtkNew, pObj);
+ pObj->pCopy->fPhase = pObj->fPhase; // needed for choices
+ }
+ // relink the choice nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ if ( pObj->pData )
+ pObj->pCopy->pData = ((Abc_Obj_t *)pObj->pData)->pCopy;
Vec_PtrFree( vNodes );
// start the storage for initial states
- pNtkNew->vInits = Vec_IntStart( Abc_NtkObjNumMax(pNtkNew) );
+ pNtkNew->vInits = Vec_IntStart( 2 * Abc_NtkObjNumMax(pNtkNew) );
// reconnect the internal nodes
- Abc_AigForEachAnd( pNtk, pObj, i )
- {
- // 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 );
- }
- // reconnect the POs
- Abc_NtkForEachPo( pNtk, pObj, i )
+ Abc_NtkForEachObj( pNtk, pObj, i )
{
- // 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 );
+ // skip the constant and the PIs
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ continue;
+ // process the first fanin
+ pFanin = Abc_NodeAigToSeq( pObj, 0, &nLatches, &Init );
+ Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
+ Abc_ObjAddFaninL0( pObj->pCopy, nLatches );
+ Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 0, Init );
+ if ( Abc_ObjFaninNum(pObj) == 1 )
+ continue;
+ // process the second fanin
+ pFanin = Abc_NodeAigToSeq( pObj, 1, &nLatches, &Init );
+ Abc_ObjAddFanin( pObj->pCopy, Abc_ObjGetCopy(pFanin) );
+ Abc_ObjAddFaninL1( pObj->pCopy, nLatches );
+ Vec_IntWriteEntry( pNtkNew->vInits, 2 * i + 1, Init );
}
// set the cutset composed of latch drivers
pNtkNew->vLats = Abc_NtkAigCutsetCopy( pNtk );
@@ -170,24 +177,31 @@ Vec_Ptr_t * Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, int * pnInit )
+Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, unsigned * pnInit )
{
Abc_Obj_t * pFanin;
- int Init;
+ Abc_InitType_t Init;
// get the given fanin of the node
pFanin = Abc_ObjFanin( pObj, Num );
if ( !Abc_ObjIsLatch(pFanin) )
{
- *pnLatches = *pnInit = 0;
+ *pnLatches = 0;
+ *pnInit = 0;
return Abc_ObjChild( pObj, Num );
}
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;
+ if ( Abc_ObjIsComplement(pFanin) )
+ {
+ if ( Init == ABC_INIT_ZERO )
+ Init = ABC_INIT_ONE;
+ else if ( Init == ABC_INIT_ONE )
+ Init = ABC_INIT_ZERO;
+ else if ( Init != ABC_INIT_DC )
+ assert( 0 );
+ }
// update the latch number and initial state
(*pnLatches)++;
(*pnInit) = ((*pnInit) << 2) | Init;
@@ -195,6 +209,120 @@ Abc_Obj_t * Abc_NodeAigToSeq( Abc_Obj_t * pObj, int Num, int * pnLatches, int *
}
+
+
+/**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;
+ int i, nCutNodes, nDigits;
+ unsigned Init;
+ assert( Abc_NtkIsSeq(pNtk) );
+ // start the network without latches
+ nCutNodes = pNtk->vLats->nSize; pNtk->vLats->nSize = 0;
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_SOP );
+ pNtk->vLats->nSize = nCutNodes;
+ // create the constant node
+ Abc_NtkDupConst1( pNtk, pNtkNew );
+ // duplicate the nodes, create node functions
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ // skip the constant
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ continue;
+ // duplicate the node
+ Abc_NtkDupObj(pNtkNew, pObj);
+ if ( Abc_ObjFaninNum(pObj) == 1 )
+ {
+ assert( !Abc_ObjFaninC0(pObj) );
+ pObj->pCopy->pData = Abc_SopCreateBuf( pNtkNew->pManFunc );
+ continue;
+ }
+ pObj->pCopy->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+ }
+ // connect the objects
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ // skip PIs and the constant
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ continue;
+ // get the initial states of the latches on the fanin edge of this node
+ Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id );
+ // create the edge
+ pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninL0(pObj), Init );
+ Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+ if ( Abc_ObjFaninNum(pObj) == 1 )
+ {
+ // create the complemented edge
+ if ( Abc_ObjFaninC0(pObj) )
+ Abc_ObjSetFaninC( pObj->pCopy, 0 );
+ continue;
+ }
+ // get the initial states of the latches on the fanin edge of this node
+ Init = Vec_IntEntry( pNtk->vInits, 2 * pObj->Id + 1 );
+ // create the edge
+ pFaninNew = Abc_NodeSeqToLogic( pNtkNew, Abc_ObjFanin1(pObj), Abc_ObjFaninL1(pObj), Init );
+ Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+ // the complemented edges are subsumed by the node function
+ }
+ // 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
+ Abc_NtkLogicStoreName( pObjNew, Abc_ObjNameDummy("L", i, nDigits) );
+ }
+ // 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, unsigned 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/abcShare.c b/src/base/abcs/abcShare.c
new file mode 100644
index 00000000..4f12b7bc
--- /dev/null
+++ b/src/base/abcs/abcShare.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+ FileName [abcShare.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Procedures for latch sharing on the fanout edges.]
+
+ Synopsis [Utilities working sequential AIGs.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcShare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abcs.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+static void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, int Init, Vec_Ptr_t * vNodes );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the sequential AIG to take fanout sharing into account.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ int i;
+ vNodes = Vec_PtrAlloc( 10 );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ Abc_NodeSeqShareFanouts( pObj, vNodes );
+ Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the node to take fanout sharing into account.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeSeqShareFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+ Abc_Obj_t * pFanout;
+ Abc_InitType_t Type;
+ int nLatches[4], i;
+ // skip the node with only one fanout
+ if ( Abc_ObjFanoutNum(pNode) < 2 )
+ return;
+ // clean the the fanout counters
+ for ( i = 0; i < 4; i++ )
+ nLatches[i] = 0;
+ // find the number of fanouts having latches of each type
+ Abc_ObjForEachFanout( pNode, pFanout, i )
+ {
+ if ( Abc_ObjFanoutL(pNode, pFanout) == 0 )
+ continue;
+ Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
+ nLatches[Type]++;
+ }
+ // decide what to do
+ if ( nLatches[ABC_INIT_ZERO] > 1 && nLatches[ABC_INIT_ONE] > 1 ) // 0-group and 1-group
+ {
+ Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+ Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE, vNodes ); // shares 1 and DC
+ }
+ else if ( nLatches[ABC_INIT_ZERO] > 1 ) // 0-group
+ Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+ else if ( nLatches[ABC_INIT_ONE] > 1 ) // 1-group
+ Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE, vNodes ); // shares 1 and DC
+ else if ( nLatches[ABC_INIT_DC] > 1 ) // DC-group
+ {
+ if ( nLatches[ABC_INIT_ZERO] > 0 )
+ Abc_NodeSeqShareOne( pNode, ABC_INIT_ZERO, vNodes ); // shares 0 and DC
+ else
+ Abc_NodeSeqShareOne( pNode, ABC_INIT_ONE, vNodes ); // shares 1 and DC
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the node to take fanout sharing into account.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeSeqShareOne( Abc_Obj_t * pNode, Abc_InitType_t Init, Vec_Ptr_t * vNodes )
+{
+ Vec_Int_t * vInits = pNode->pNtk->vInits;
+ Abc_Obj_t * pFanout, * pBuffer;
+ Abc_InitType_t Type, InitNew;
+ int i;
+ // collect the fanouts that satisfy the property (have initial value Init or DC)
+ InitNew = ABC_INIT_DC;
+ Vec_PtrClear( vNodes );
+ Abc_ObjForEachFanout( pNode, pFanout, i )
+ {
+ Type = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
+ if ( Type == Init )
+ InitNew = Init;
+ if ( Type == Init || Type == ABC_INIT_DC )
+ {
+ Vec_PtrPush( vNodes, pFanout );
+ Abc_ObjFaninLDeleteLast( pFanout, Abc_ObjEdgeNum(pNode, pFanout) );
+ }
+ }
+ // create the new buffer
+ pBuffer = Abc_NtkCreateNode( pNode->pNtk );
+ Abc_ObjAddFanin( pBuffer, pNode );
+ Abc_ObjSetFaninL( pBuffer, 0, 1 );
+ // add the initial state
+ assert( Vec_IntSize(vInits) == 2 * (int)pBuffer->Id );
+ Vec_IntPush( vInits, InitNew );
+ Vec_IntPush( vInits, 0 );
+ // redirect the fanouts
+ Vec_PtrForEachEntry( vNodes, pFanout, i )
+ Abc_ObjPatchFanin( pFanout, pNode, pBuffer );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abcs/abcUtils.c b/src/base/abcs/abcUtils.c
index 8dccb81d..a9f3254c 100644
--- a/src/base/abcs/abcUtils.c
+++ b/src/base/abcs/abcUtils.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "abc.h"
+#include "abcs.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -30,166 +30,7 @@
/**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.]
+ Synopsis [Counts the number of latches in the sequential AIG.]
Description []
@@ -213,7 +54,7 @@ int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk )
/**Function*************************************************************
- Synopsis [Counters the number of latches in the sequential AIG.]
+ Synopsis [Counts the number of latches in the sequential AIG.]
Description []
diff --git a/src/base/abcs/abcs.h b/src/base/abcs/abcs.h
new file mode 100644
index 00000000..bfa95f3e
--- /dev/null
+++ b/src/base/abcs/abcs.h
@@ -0,0 +1,315 @@
+/**CFile****************************************************************
+
+ FileName [abcs.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential synthesis package.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __ABCS_H__
+#define __ABCS_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+// the maximum number of latches on the edge
+#define ABC_MAX_EDGE_LATCH 16
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// representation of latch on the edge
+typedef struct Abc_RetEdge_t_ Abc_RetEdge_t;
+struct Abc_RetEdge_t_ // 1 word
+{
+ unsigned iNode : 24; // the ID of the node
+ unsigned iEdge : 1; // the edge of the node
+ unsigned iLatch : 7; // the latch number counting from the node
+};
+
+// representation of one retiming step
+typedef struct Abc_RetStep_t_ Abc_RetStep_t;
+struct Abc_RetStep_t_ // 1 word
+{
+ unsigned iNode : 24; // the ID of the node
+ unsigned nLatches : 8; // the number of latches to retime
+};
+
+static inline int Abc_RetEdge2Int( Abc_RetEdge_t Str ) { return *((int *)&Str); }
+static inline Abc_RetEdge_t Abc_Int2RetEdge( int Num ) { return *((Abc_RetEdge_t *)&Num); }
+
+static inline int Abc_RetStep2Int( Abc_RetStep_t Str ) { return *((int *)&Str); }
+static inline Abc_RetStep_t Abc_Int2RetStep( int Num ) { return *((Abc_RetStep_t *)&Num); }
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// getting the number of the edge for this fanout
+static inline int Abc_ObjEdgeNum( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )
+{
+ assert( Abc_NtkIsSeq(pObj->pNtk) );
+ if ( Abc_ObjFaninId0(pFanout) == (int)pObj->Id )
+ return 0;
+ else if ( Abc_ObjFaninId1(pFanout) == (int)pObj->Id )
+ return 1;
+ assert( 0 );
+ return -1;
+}
+
+// getting the latch number of the fanout
+static inline int Abc_ObjFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout )
+{
+ return Abc_ObjFaninL( pFanout, Abc_ObjEdgeNum(pObj,pFanout) );
+}
+
+// setting the latch number of the fanout
+static inline void Abc_ObjSetFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )
+{
+ Abc_ObjSetFaninL( pFanout, Abc_ObjEdgeNum(pObj,pFanout), nLats );
+}
+
+// adding to the latch number of the fanout
+static inline void Abc_ObjAddFanoutL( Abc_Obj_t * pObj, Abc_Obj_t * pFanout, int nLats )
+{
+ Abc_ObjAddFaninL( pFanout, Abc_ObjEdgeNum(pObj,pFanout), nLats );
+}
+
+// returns the latch number of the fanout
+static inline 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;
+}
+
+// returns the latch number of the fanout
+static inline 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;
+}
+
+// returns the sum of latches on the fanout edges
+static inline 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;
+}
+
+// returns the sum of latches on the fanin edges
+static inline 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;
+}
+
+
+// getting the bit-string of init values of the edge
+static inline unsigned Abc_ObjFaninLGetInit( Abc_Obj_t * pObj, int Edge )
+{
+ return (unsigned)Vec_IntEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge );
+}
+
+// setting bit-string of init values of the edge
+static inline void Abc_ObjFaninLSetInit( Abc_Obj_t * pObj, int Edge, unsigned Init )
+{
+ Vec_IntWriteEntry( pObj->pNtk->vInits, 2 * pObj->Id + Edge, Init );
+}
+
+// setting the init value of the given latch on the edge
+static inline void Abc_ObjFaninLSetInitOne( Abc_Obj_t * pObj, int Edge, int iLatch, Abc_InitType_t Init )
+{
+ unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+ unsigned EntryNew = (EntryCur & ~(0x3 << iLatch)) | (Init << iLatch);
+ assert( iLatch < Abc_ObjFaninL(pObj, Edge) );
+ Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+}
+
+// geting the init value of the first latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLGetInitFirst( Abc_Obj_t * pObj, int Edge )
+{
+ return 0x3 & Abc_ObjFaninLGetInit( pObj, Edge );
+}
+
+// geting the init value of the last latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLGetInitLast( Abc_Obj_t * pObj, int Edge )
+{
+ assert( Abc_ObjFaninL(pObj, Edge) > 0 );
+ return 0x3 & (Abc_ObjFaninLGetInit(pObj, Edge) >> (2 * (Abc_ObjFaninL(pObj, Edge) - 1)));
+}
+
+// insert the first latch on the edge
+static inline void Abc_ObjFaninLInsertFirst( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
+{
+ unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+ unsigned EntryNew = ((EntryCur << 2) | Init);
+ assert( Init >= 0 && Init < 4 );
+ assert( Abc_ObjFaninL(pObj, Edge) < ABC_MAX_EDGE_LATCH );
+ Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+ Abc_ObjAddFaninL( pObj, Edge, 1 );
+}
+
+// insert the last latch on the edge
+static inline void Abc_ObjFaninLInsertLast( Abc_Obj_t * pObj, int Edge, Abc_InitType_t Init )
+{
+ unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+ unsigned EntryNew = EntryCur | (Init << (2 * Abc_ObjFaninL(pObj, Edge)));
+ assert( Init >= 0 && Init < 4 );
+ assert( Abc_ObjFaninL(pObj, Edge) < ABC_MAX_EDGE_LATCH );
+ Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+ Abc_ObjAddFaninL( pObj, Edge, 1 );
+}
+
+// delete the first latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLDeleteFirst( Abc_Obj_t * pObj, int Edge )
+{
+ unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+ Abc_InitType_t Init = 0x3 & EntryCur;
+ unsigned EntryNew = EntryCur >> 2;
+ assert( Abc_ObjFaninL(pObj, Edge) > 0 );
+ Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+ Abc_ObjAddFaninL( pObj, Edge, -1 );
+ return Init;
+}
+
+// delete the last latch on the edge
+static inline Abc_InitType_t Abc_ObjFaninLDeleteLast( Abc_Obj_t * pObj, int Edge )
+{
+ unsigned EntryCur = Abc_ObjFaninLGetInit(pObj, Edge);
+ Abc_InitType_t Init = 0x3 & (EntryCur >> (2 * (Abc_ObjFaninL(pObj, Edge) - 1)));
+ unsigned EntryNew = EntryCur & ~(((unsigned)0x3) << (2 * (Abc_ObjFaninL(pObj, Edge)-1)));
+ assert( Abc_ObjFaninL(pObj, Edge) > 0 );
+ Abc_ObjFaninLSetInit( pObj, Edge, EntryNew );
+ Abc_ObjAddFaninL( pObj, Edge, -1 );
+ return Init;
+}
+
+// retime node forward without initial states
+static inline 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( Abc_ObjFaninL0(pObj) >= nLatches );
+ assert( Abc_ObjFaninL1(pObj) >= nLatches );
+ // subtract these latches on the fanin side
+ Abc_ObjAddFaninL0( pObj, -nLatches );
+ Abc_ObjAddFaninL1( pObj, -nLatches );
+ // add these latches on the fanout size
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ Abc_ObjAddFanoutL( pObj, pFanout, nLatches );
+}
+
+// retime node backward without initial states
+static inline 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 );
+ // subtract these latches on the fanout side
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ {
+ assert( Abc_ObjFanoutL(pObj, pFanout) >= nLatches );
+ Abc_ObjAddFanoutL( pObj, pFanout, -nLatches );
+ }
+ // add these latches on the fanin size
+ Abc_ObjAddFaninL0( pObj, nLatches );
+ Abc_ObjAddFaninL1( pObj, nLatches );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+// iterating through the initial values of the edge
+#define Abc_ObjFaninLForEachValue( pObj, Edge, Init, i, Value ) \
+ for ( i = 0, Init = Abc_ObjFaninLGetInit(pObj, Edge); \
+ i < Abc_ObjFaninL(pObj, Edge) && ((Value = ((Init >> i) & 3)), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== abcRetCore.c ===========================================================*/
+extern void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk );
+extern void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk );
+extern void Abc_NtkSeqRetimeInitial( Abc_Ntk_t * pNtk );
+extern void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk );
+/*=== abcRetDelay.c ==========================================================*/
+extern Vec_Str_t * Abc_NtkSeqRetimeDelayLags( Abc_Ntk_t * pNtk );
+/*=== abcRetImpl.c ===========================================================*/
+extern int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags );
+extern void Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+extern int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves );
+/*=== abcRetUtil.c ===========================================================*/
+extern Vec_Ptr_t * Abc_NtkUtilRetimingTry( Abc_Ntk_t * pNtk, bool fForward );
+extern Vec_Ptr_t * Abc_NtkUtilRetimingGetMoves( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, bool fForward );
+extern Vec_Int_t * Abc_NtkUtilRetimingSplit( Vec_Str_t * vLags, int fForward );
+/*=== abcSeq.c ===============================================================*/
+extern Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk );
+/*=== abcShare.c =============================================================*/
+extern void Abc_NtkSeqShareFanouts( Abc_Ntk_t * pNtk );
+/*=== abcUtil.c ==============================================================*/
+extern int Abc_NtkSeqLatchNum( Abc_Ntk_t * pNtk );
+extern int Abc_NtkSeqLatchNumShared( Abc_Ntk_t * pNtk );
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 393b2216..988cabfb 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -114,7 +114,10 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
// get the node name and the node type
pType = vTokens->pArray[1];
if ( strcmp(pType, "DFF") == 0 )
- Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
+ {
+ pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] );
+ Abc_LatchSetInit0( pNode );
+ }
else
{
// create a new node and add it to the network
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 7adec714..1cae68e7 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -395,7 +395,6 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
Abc_Ntk_t * pNtk = p->pNtk;
Abc_Obj_t * pLatch;
int ResetValue;
-
if ( vTokens->nSize < 3 )
{
p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -407,7 +406,7 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
pLatch = Io_ReadCreateLatch( pNtk, vTokens->pArray[1], vTokens->pArray[2] );
// get the latch reset value
if ( vTokens->nSize == 3 )
- ResetValue = 2;
+ Abc_LatchSetInitDc( pLatch );
else
{
ResetValue = atoi(vTokens->pArray[3]);
@@ -418,8 +417,13 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
Io_ReadBlifPrintErrorMessage( p );
return 1;
}
+ if ( ResetValue == 0 )
+ Abc_LatchSetInit0( pLatch );
+ else if ( ResetValue == 1 )
+ Abc_LatchSetInit1( pLatch );
+ else if ( ResetValue == 2 )
+ Abc_LatchSetInitDc( pLatch );
}
- Abc_ObjSetData( pLatch, (void *)ResetValue );
return 0;
}
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 48a1722b..d94b46c7 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -114,7 +114,10 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
vTokens = Extra_FileReaderGetTokens(p);
pGateName = vTokens->pArray[1];
if ( strncmp( pGateName, "Flip", 4 ) == 0 )
+ {
pObj = Abc_NtkCreateLatch( pNtk );
+ Abc_LatchSetInit0( pObj );
+ }
else
{
pObj = Abc_NtkCreateNode( pNtk );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 132684cc..e3e9c59a 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -82,7 +82,7 @@ Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName )
Synopsis [Create a latch with the given input/output.]
- Description []
+ Description [By default, the latch value is unknown (ABC_INIT_NONE).]
SideEffects []
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 7d6815b9..84fedc34 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -300,7 +300,7 @@ void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
fprintf( pFile, ".latch" );
fprintf( pFile, " %10s", Abc_ObjName(pNetLi) );
fprintf( pFile, " %10s", Abc_ObjName(pNetLo) );
- fprintf( pFile, " %d\n", Reset );
+ fprintf( pFile, " %d\n", Reset-1 );
}
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 4481297a..37822383 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -515,7 +515,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
if ( mng->mode == 0 ) // brute-force SAT
{
- // transfor the AIG into a logic network for efficient CNF construction
+ // transform the AIG into a logic network for efficient CNF construction
pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 );
RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 );