luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc50813

This commit is contained in:
Alan Mishchenko 2005-08-13 08:01:00 -07:00
parent 80983617b3
commit f2b6b3be95
13 changed files with 1542 additions and 147 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
abc.dsp
View File

@ -197,6 +197,14 @@ SOURCE=.\src\base\abc\abcSat.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcSeq.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcSeqRetime.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcShow.c
# End Source File
# Begin Source File

BIN
abc.opt
View File

Binary file not shown.

28
abc.plg
View File

@ -6,13 +6,13 @@
--------------------Configuration: abc - Win32 Debug--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DC.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60E.tmp" with contents
[
/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /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\abc\abcMap.c"
"C:\_projects\abc\src\base\abc\abc.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DC.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DD.tmp" with contents
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60E.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60F.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\abc.obj
@ -59,6 +59,8 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\ioReadBlif.obj
.\Debug\ioReadPla.obj
.\Debug\ioReadVerilog.obj
.\Debug\ioUtil.obj
.\Debug\ioWriteBench.obj
.\Debug\ioWriteBlif.obj
.\Debug\ioWriteCnf.obj
.\Debug\ioWritePla.obj
@ -264,15 +266,15 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\safe_mem.obj
.\Debug\strsav.obj
.\Debug\texpand.obj
.\Debug\ioUtil.obj
.\Debug\ioWriteBench.obj
.\Debug\abcSeq.obj
.\Debug\abcSeqRetime.obj
]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DD.tmp"
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP60F.tmp"
<h3>Output Window</h3>
Compiling...
abcMap.c
abc.c
Linking...
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DE.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp" with contents
[
/nologo /o"Debug/abc.bsc"
.\Debug\abc.sbr
@ -319,6 +321,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DE.tmp" with conte
.\Debug\ioReadBlif.sbr
.\Debug\ioReadPla.sbr
.\Debug\ioReadVerilog.sbr
.\Debug\ioUtil.sbr
.\Debug\ioWriteBench.sbr
.\Debug\ioWriteBlif.sbr
.\Debug\ioWriteCnf.sbr
.\Debug\ioWritePla.sbr
@ -524,9 +528,9 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DE.tmp" with conte
.\Debug\safe_mem.sbr
.\Debug\strsav.sbr
.\Debug\texpand.sbr
.\Debug\ioUtil.sbr
.\Debug\ioWriteBench.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4DE.tmp"
.\Debug\abcSeq.sbr
.\Debug\abcSeqRetime.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP610.tmp"
Creating browse info file...
<h3>Output Window</h3>

161
src/base/abc/abc.c
View File

@ -69,6 +69,9 @@ static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -130,6 +133,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga", Abc_CommandFpga, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
@ -170,21 +176,26 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
bool fShort;
int c;
int fFactor;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set the defaults
fShort = 1;
fShort = 1;
fFactor = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "sfh" ) ) != EOF )
{
switch ( c )
{
case 's':
fShort ^= 1;
break;
case 'f':
fFactor ^= 1;
break;
case 'h':
goto usage;
default:
@ -197,12 +208,13 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( Abc_FrameReadErr(pAbc), "Empty network\n" );
return 1;
}
Abc_NtkPrintStats( pOut, pNtk );
Abc_NtkPrintStats( pOut, pNtk, fFactor );
return 0;
usage:
fprintf( pErr, "usage: print_stats [-h]\n" );
fprintf( pErr, "usage: print_stats [-fh]\n" );
fprintf( pErr, "\t prints the network statistics and\n" );
fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -2799,6 +2811,147 @@ usage:
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsAig(pNtk) )
{
fprintf( pErr, "Works only for AIG.\n" );
return 1;
}
// get the new network
pNtkRes = Abc_NtkAigToSeq( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Converting to sequential AIG has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: seq [-h]\n" );
fprintf( pErr, "\t converts AIG into sequential AIG (while sweeping latches)\n" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
int fForward;
int fBackward;
extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
fForward = 0;
fBackward = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "fbh" ) ) != EOF )
{
switch ( c )
{
case 'f':
fForward ^= 1;
break;
case 'b':
fBackward ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsSeq(pNtk) )
{
fprintf( pErr, "Works only for sequential AIG.\n" );
return 1;
}
// get the new network
if ( fForward )
Abc_NtkSeqRetimeForward( pNtk );
else if ( fBackward )
Abc_NtkSeqRetimeBackward( 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, "\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-h : print the command usage\n");
return 1;
}
/**Function*************************************************************

92
src/base/abc/abc.h
View File

@ -143,6 +143,7 @@ struct Abc_Ntk_t_
Vec_Ptr_t * vPtrTemp; // the temporary array
Vec_Int_t * vIntTemp; // the temporary array
Vec_Str_t * vStrTemp; // the temporary array
void * pData; // the temporary pointer
// the backup network and the step number
Abc_Ntk_t * pNetBackup; // the pointer to the previous backup network
int iStep; // the generation number for the given network
@ -180,6 +181,11 @@ struct Abc_ManRes_t_
/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
// maximum/minimum operators
#define ABC_MIN(a,b) (((a) < (b))? (a) : (b))
#define ABC_MAX(a,b) (((a) > (b))? (a) : (b))
#define ABC_INFINITY (10000000)
// reading data members of the network
static inline char * Abc_NtkName( Abc_Ntk_t * pNtk ) { return pNtk->pName; }
static inline char * Abc_NtkSpec( Abc_Ntk_t * pNtk ) { return pNtk->pSpec; }
@ -247,31 +253,6 @@ static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p ) { return (Abc_
static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p ) { return (Abc_Obj_t *)((unsigned)(p) ^ 01); }
static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c ) { return (Abc_Obj_t *)((unsigned)(p) ^ (c)); }
// working with fanin/fanout edges
static inline int Abc_ObjFaninNum( Abc_Obj_t * pObj ) { return pObj->vFanins.nSize; }
static inline int Abc_ObjFanoutNum( Abc_Obj_t * pObj ) { return pObj->vFanouts.nSize; }
static inline int Abc_ObjFaninId( Abc_Obj_t * pObj, int i){ return pObj->vFanins.pArray[i].iFan; }
static inline int Abc_ObjFaninId0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].iFan; }
static inline int Abc_ObjFaninId1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].iFan; }
static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ){ return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj; }
static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl; }
static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].fCompl; }
static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].fCompl; }
static inline int Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats; }
static inline int Abc_ObjFaninL0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].nLats; }
static inline int Abc_ObjFaninL1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].nLats; }
static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );}
static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) );}
static inline void Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1; }
static inline void Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1; }
static inline void Abc_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats ) { pObj->vFanins.pArray[i].nLats = nLats; }
static inline void Abc_ObjAddFaninL( Abc_Obj_t * pObj, int i, int nLats ) { pObj->vFanins.pArray[i].nLats += nLats; }
// checking the object type
static inline bool Abc_ObjIsNode( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NODE; }
static inline bool Abc_ObjIsNet( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NET; }
@ -283,6 +264,43 @@ static inline bool Abc_ObjIsCi( Abc_Obj_t * pObj ) { return pObj-
static inline bool Abc_ObjIsCo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
static inline bool Abc_ObjIsCio( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
// working with fanin/fanout edges
static inline int Abc_ObjFaninNum( Abc_Obj_t * pObj ) { return pObj->vFanins.nSize; }
static inline int Abc_ObjFanoutNum( Abc_Obj_t * pObj ) { return pObj->vFanouts.nSize; }
static inline int Abc_ObjFaninId( Abc_Obj_t * pObj, int i){ return pObj->vFanins.pArray[i].iFan; }
static inline int Abc_ObjFaninId0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].iFan; }
static inline int Abc_ObjFaninId1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].iFan; }
static inline Abc_Obj_t * Abc_ObjFanout( Abc_Obj_t * pObj, int i ){ return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanouts.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj ) { return pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1].iFan ]; }
static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj ) { return Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj) : pObj; }
static inline bool Abc_ObjFaninC( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].fCompl; }
static inline bool Abc_ObjFaninC0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].fCompl; }
static inline bool Abc_ObjFaninC1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].fCompl; }
static inline int Abc_ObjFaninL( Abc_Obj_t * pObj, int i ){ return pObj->vFanins.pArray[i].nLats; }
static inline int Abc_ObjFaninL0( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[0].nLats; }
static inline int Abc_ObjFaninL1( Abc_Obj_t * pObj ) { return pObj->vFanins.pArray[1].nLats; }
static inline int Abc_ObjFaninLMin( Abc_Obj_t * pObj ) { assert( Abc_ObjIsNode(pObj) ); return ABC_MIN( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
static inline int Abc_ObjFaninLMax( Abc_Obj_t * pObj ) { assert( Abc_ObjIsNode(pObj) ); return ABC_MAX( Abc_ObjFaninL0(pObj), Abc_ObjFaninL1(pObj) ); }
static inline Abc_Obj_t * Abc_ObjChild( Abc_Obj_t * pObj, int i ) { return Abc_ObjNotCond( Abc_ObjFanin(pObj,i), Abc_ObjFaninC(pObj,i) );}
static inline Abc_Obj_t * Abc_ObjChild0( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) ); }
static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj), Abc_ObjFaninC1(pObj) ); }
static inline void Abc_ObjSetFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl = 1; }
static inline void Abc_ObjXorFaninC( Abc_Obj_t * pObj, int i ){ pObj->vFanins.pArray[i].fCompl ^= 1; }
static inline void Abc_ObjSetFaninL( Abc_Obj_t * pObj, int i, int nLats ) { pObj->vFanins.pArray[i].nLats = nLats; }
static inline void Abc_ObjSetFaninL0( Abc_Obj_t * pObj, int nLats ) { pObj->vFanins.pArray[0].nLats = nLats; }
static inline void Abc_ObjSetFaninL1( Abc_Obj_t * pObj, int nLats ) { pObj->vFanins.pArray[1].nLats = 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 );
// checking the node type
static inline bool Abc_NodeIsAigAnd( Abc_Obj_t * pNode ) { assert(Abc_NtkIsAig(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2; }
static inline bool Abc_NodeIsAigChoice( Abc_Obj_t * pNode ){ assert(Abc_NtkIsAig(pNode->pNtk)); return pNode->pData != NULL && Abc_ObjFanoutNum(pNode) > 0; }
@ -299,11 +317,6 @@ static inline void Abc_NodeSetTravIdPrevious( Abc_Obj_t * pNode ) { p
static inline bool Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode ) { return (bool)(pNode->TravId == pNode->pNtk->nTravIds); }
static inline bool Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode ) { return (bool)(pNode->TravId == pNode->pNtk->nTravIds - 1); }
// maximum/minimum operators
#define ABC_MIN(a,b) (((a) < (b))? (a) : (b))
#define ABC_MAX(a,b) (((a) > (b))? (a) : (b))
#define ABC_INFINITY (10000000)
// outputs the runtime in seconds
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
@ -356,13 +369,18 @@ static inline bool Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode ) { r
////////////////////////////////////////////////////////////////////////
/*=== abcAig.c ==========================================================*/
extern Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtk );
extern Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtk, bool fSeq );
extern Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, bool fSeq );
extern void Abc_AigFree( Abc_Aig_t * pMan );
extern int Abc_AigCleanup( Abc_Aig_t * pMan );
extern bool Abc_AigCheck( Abc_Aig_t * pMan );
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_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew );
extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
/*=== abcAttach.c ==========================================================*/
@ -378,6 +396,7 @@ extern void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNt
extern Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type );
extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type );
extern void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkStartRead( char * pName );
extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk );
@ -385,6 +404,8 @@ extern Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNod
extern void Abc_NtkDelete( Abc_Ntk_t * pNtk );
extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
extern Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew );
extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
@ -462,7 +483,7 @@ extern Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
/*=== abcPrint.c ==========================================================*/
extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored );
extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
@ -481,6 +502,13 @@ extern void Abc_NtkManResStop( Abc_ManRes_t * p );
/*=== abcSat.c ==========================================================*/
extern bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, 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 );
extern void Abc_NtkSeqRetimeForward( Abc_Ntk_t * pNtk );
extern void Abc_NtkSeqRetimeBackward( Abc_Ntk_t * pNtk );
extern void Abc_NtkSeqRetimeDelay( 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 );

535
src/base/abc/abcAig.c
View File

@ -20,6 +20,23 @@
#include "abc.h"
/*
AIG is an And-Inv Graph with structural hashing.
It is always structurally hashed. It means that at any time:
- the constants are propagated
- there is no single-input nodes (inverters/buffers)
- for each AND gate, there are no other AND gates with the same children.
The operations that are performed on AIG:
- building new nodes (Abc_AigAnd)
- elementary Boolean operations (Abc_AigOr, Abc_AigXor, etc)
- propagation of constants (Abc_AigReplace)
- variable substitution (Abc_AigReplace)
When AIG is duplicated, the new graph is struturally hashed too.
If this repeated hashing leads to fewer nodes, it means the original
AIG was not strictly hashed (using the three criteria above).
*/
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -27,12 +44,16 @@
// the simple AIG manager
struct Abc_Aig_t_
{
Abc_Ntk_t * pAig; // the AIG network
Abc_Obj_t * pConst1; // the constant 1 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
Vec_Ptr_t * vNodes; // the temporary array of nodes
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 ** pBins; // the table bins
int nBins; // the size of the table
int nEntries; // the total number of entries in the table
Vec_Ptr_t * vNodes; // the temporary array of nodes
Vec_Ptr_t * vStackDelete; // the nodes to be deleted
Vec_Ptr_t * vStackReplaceOld; // the nodes to be replaced
Vec_Ptr_t * vStackReplaceNew; // the nodes to be used for replacement
};
// iterators through the entries in the linked lists of nodes
@ -51,8 +72,15 @@ struct Abc_Aig_t_
static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
//static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
// static hash table procedures
static void Abc_AigResize( Abc_Aig_t * pMan );
// structural hash table procedures
static Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd );
static Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
static void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis );
static void Abc_AigResize( Abc_Aig_t * pMan );
// incremental AIG procedures
static void Abc_AigReplace_int( Abc_Aig_t * pMan );
static void Abc_AigDelete_int( Abc_Aig_t * pMan );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
@ -69,7 +97,7 @@ static void Abc_AigResize( Abc_Aig_t * pMan );
SeeAlso []
***********************************************************************/
Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig, bool fSeq )
{
Abc_Aig_t * pMan;
// start the manager
@ -80,12 +108,36 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
pMan->pBins = ALLOC( Abc_Obj_t *, pMan->nBins );
memset( pMan->pBins, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
pMan->vNodes = Vec_PtrAlloc( 100 );
pMan->vStackDelete = Vec_PtrAlloc( 100 );
pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
// save the current network
pMan->pAig = pNtkAig;
pMan->pConst1 = Abc_NtkCreateNode( pNtkAig );
pMan->pNtkAig = pNtkAig;
pMan->pConst1 = Abc_NtkCreateNode( pNtkAig );
pMan->pReset = fSeq? Abc_NtkCreateNode( pNtkAig ) : NULL;
return pMan;
}
/**Function*************************************************************
Synopsis [Duplicated the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, bool fSeq )
{
Abc_Aig_t * pManNew;
pManNew = Abc_AigAlloc( pMan->pNtkAig, fSeq );
return pManNew;
}
/**Function*************************************************************
Synopsis [Deallocates the local AIG manager.]
@ -99,12 +151,102 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
***********************************************************************/
void Abc_AigFree( Abc_Aig_t * pMan )
{
assert( Vec_PtrSize( pMan->vStackDelete ) == 0 );
assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 );
assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 );
// free the table
Vec_PtrFree( pMan->vStackDelete );
Vec_PtrFree( pMan->vStackReplaceOld );
Vec_PtrFree( pMan->vStackReplaceNew );
Vec_PtrFree( pMan->vNodes );
free( pMan->pBins );
free( pMan );
}
/**Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_AigCleanup( Abc_Aig_t * pMan )
{
Abc_Obj_t * pAnd;
int i, Counter;
// collect the AND nodes that do not fanout
assert( Vec_PtrSize( pMan->vStackDelete ) == 0 );
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
if ( Abc_ObjFanoutNum(pAnd) == 0 )
Vec_PtrPush( pMan->vStackDelete, pAnd );
// process the dangling nodes and their MFFCs
for ( Counter = 0; Vec_PtrSize(pMan->vStackDelete) > 0; Counter++ )
Abc_AigDelete_int( pMan );
return Counter;
}
/**Function*************************************************************
Synopsis [Makes sure that every node in the table is in the network and vice versa.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
bool Abc_AigCheck( Abc_Aig_t * pMan )
{
Abc_Obj_t * pObj, * pAnd;
int i, nFanins, Counter;
Abc_NtkForEachNode( pMan->pNtkAig, pObj, i )
{
nFanins = Abc_ObjFaninNum(pObj);
if ( nFanins == 0 )
{
if ( pObj != pMan->pConst1 && pObj != pMan->pReset )
{
printf( "Abc_AigCheck: The AIG has non-standard constant nodes.\n" );
return 0;
}
continue;
}
if ( nFanins == 1 )
{
printf( "Abc_AigCheck: The AIG has single input nodes.\n" );
return 0;
}
if ( nFanins > 2 )
{
printf( "Abc_AigCheck: The AIG has non-standard nodes.\n" );
return 0;
}
pAnd = Abc_AigAndLookup( pMan, Abc_ObjChild0(pObj), Abc_ObjChild1(pObj) );
if ( pAnd != pObj )
{
printf( "Abc_AigCheck: Node \"%s\" is not in the structural hashing table.\n", Abc_ObjName(pObj) );
return 0;
}
}
// count the number of nodes in the table
Counter = 0;
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntry( pMan->pBins[i], pAnd )
Counter++;
if ( Counter + 1 + Abc_NtkIsSeq(pMan->pNtkAig) != Abc_NtkNodeNum(pMan->pNtkAig) )
{
printf( "Abc_AigCheck: The number of nodes in the structural hashing table is wrong.\n", Counter );
return 0;
}
return 1;
}
/**Function*************************************************************
Synopsis [Read the constant 1 node.]
@ -121,6 +263,24 @@ 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*************************************************************
Synopsis [Performs canonicization step.]
@ -132,7 +292,71 @@ Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan )
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
{
Abc_Obj_t * pAnd;
unsigned Key;
// check if it is a good time for table resizing
if ( pMan->nEntries > 2 * pMan->nBins )
Abc_AigResize( pMan );
// order the arguments
if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
pAnd = p0, p0 = p1, p1 = pAnd;
// create the new node
pAnd = Abc_NtkCreateNode( pMan->pNtkAig );
Abc_ObjAddFanin( pAnd, p0 );
Abc_ObjAddFanin( pAnd, p1 );
// set the level of the new node
pAnd->Level = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level );
// add the node to the corresponding linked list in the table
Key = Abc_HashKey2( p0, p1, pMan->nBins );
pAnd->pNext = pMan->pBins[Key];
pMan->pBins[Key] = pAnd;
pMan->nEntries++;
return pAnd;
}
/**Function*************************************************************
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd )
{
unsigned Key;
// order the arguments
if ( Abc_ObjRegular(p0)->Id > Abc_ObjRegular(p1)->Id )
pAnd = p0, p0 = p1, p1 = pAnd;
// create the new node
Abc_ObjAddFanin( pAnd, p0 );
Abc_ObjAddFanin( pAnd, p1 );
// set the level of the new node
pAnd->Level = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level );
// add the node to the corresponding linked list in the table
Key = Abc_HashKey2( p0, p1, pMan->nBins );
pAnd->pNext = pMan->pBins[Key];
pMan->pBins[Key] = pAnd;
return pAnd;
}
/**Function*************************************************************
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
{
Abc_Obj_t * pAnd;
unsigned Key;
@ -165,23 +389,106 @@ Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
Abc_ObjFaninC0(pAnd) == Abc_ObjIsComplement(p0) &&
Abc_ObjFaninC1(pAnd) == Abc_ObjIsComplement(p1) )
return pAnd;
// check if it is a good time for table resizing
if ( pMan->nEntries > 2 * pMan->nBins )
{
Abc_AigResize( pMan );
Key = Abc_HashKey2( p0, p1, pMan->nBins );
}
// create the new node
pAnd = Abc_NtkCreateNode( pMan->pAig );
Abc_ObjAddFanin( pAnd, p0 );
Abc_ObjAddFanin( pAnd, p1 );
// set the level of the new node
pAnd->Level = 1 + ABC_MAX( Abc_ObjRegular(p0)->Level, Abc_ObjRegular(p1)->Level );
// add the node to the corresponding linked list in the table
pAnd->pNext = pMan->pBins[Key];
pMan->pBins[Key] = pAnd;
pMan->nEntries++;
return pAnd;
return NULL;
}
/**Function*************************************************************
Synopsis [Deletes an AIG node from the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis )
{
Abc_Obj_t * pAnd, ** ppPlace;
unsigned Key;
assert( !Abc_ObjIsComplement(pThis) );
assert( Abc_ObjFanoutNum(pThis) == 0 );
assert( pMan->pNtkAig == pThis->pNtk );
// get the hash key for these two nodes
Key = Abc_HashKey2( Abc_ObjChild0(pThis), Abc_ObjChild1(pThis), pMan->nBins );
// find the mataching node in the table
ppPlace = pMan->pBins + Key;
Abc_AigBinForEachEntry( pMan->pBins[Key], pAnd )
if ( pAnd != pThis )
ppPlace = &pAnd->pNext;
else
{
*ppPlace = pAnd->pNext;
break;
}
assert( pAnd == pThis );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigResize( Abc_Aig_t * pMan )
{
Abc_Obj_t ** pBinsNew;
Abc_Obj_t * pEnt, * pEnt2;
int nBinsNew, Counter, i, clk;
unsigned Key;
clk = clock();
// get the new table size
nBinsNew = Cudd_PrimeCopy(2 * pMan->nBins);
// allocate a new array
pBinsNew = ALLOC( Abc_Obj_t *, nBinsNew );
memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * nBinsNew );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
{
Key = Abc_HashKey2( Abc_ObjFanin(pEnt,0), Abc_ObjFanin(pEnt,1), nBinsNew );
pEnt->pNext = pBinsNew[Key];
pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
free( pMan->pBins );
pMan->pBins = pBinsNew;
pMan->nBins = nBinsNew;
}
/**Function*************************************************************
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
{
Abc_Obj_t * pAnd;
if ( pAnd = Abc_AigAndLookup( pMan, p0, p1 ) )
return pAnd;
return Abc_AigAndCreate( pMan, p0, p1 );
}
/**Function*************************************************************
@ -243,6 +550,131 @@ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
return pMiter;
}
/**Function*************************************************************
Synopsis [Replaces one AIG node by the other.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew )
{
assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
assert( Vec_PtrSize(pMan->vStackDelete) == 0 );
Vec_PtrPush( pMan->vStackReplaceOld, pOld );
Vec_PtrPush( pMan->vStackReplaceNew, pNew );
while ( Vec_PtrSize(pMan->vStackReplaceOld) )
Abc_AigReplace_int( pMan );
while ( Vec_PtrSize(pMan->vStackDelete) )
Abc_AigDelete_int( pMan );
}
/**Function*************************************************************
Synopsis [Performs internal replacement step.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigReplace_int( Abc_Aig_t * pMan )
{
Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew;
int k, iFanin;
// get the pair of nodes to replace
assert( Vec_PtrSize(pMan->vStackReplaceOld) > 0 );
pOld = Vec_PtrPop( pMan->vStackReplaceOld );
pNew = Vec_PtrPop( pMan->vStackReplaceNew );
// make sure the old node is regular and has fanouts
// the new node can be complemented and can have fanouts
assert( !Abc_ObjIsComplement(pOld) == 0 );
assert( Abc_ObjFanoutNum(pOld) > 0 );
// look at the fanouts of old node
Abc_NodeCollectFanouts( pOld, pMan->vNodes );
Vec_PtrForEachEntry( pMan->vNodes, pFanout, k )
{
if ( Abc_ObjIsCo(pFanout) )
{
Abc_ObjPatchFanin( pFanout, pOld, pNew );
continue;
}
// find the old node as a fanin of this fanout
iFanin = Vec_FanFindEntry( &pFanout->vFanins, pOld->Id );
assert( iFanin == 0 || iFanin == 1 );
// get the new fanin
pFanin1 = Abc_ObjNotCond( pNew, Abc_ObjFaninC(pFanout, iFanin) );
// get another fanin
pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
// check if the node with these fanins exists
if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
{ // such node exists (it may be a constant)
// schedule replacement of the old fanout by the new fanout
Vec_PtrPush( pMan->vStackReplaceOld, pFanout );
Vec_PtrPush( pMan->vStackReplaceNew, pFanoutNew );
continue;
}
// such node does not exist - modify the old fanout
// remove the old fanout from the table
Abc_AigAndDelete( pMan, pFanout );
// remove its old fanins
Abc_ObjRemoveFanins( pFanout );
// update the old fanout with new fanins and add it to the table
Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout );
}
// schedule deletion of the old node
Vec_PtrPush( pMan->vStackDelete, pOld );
}
/**Function*************************************************************
Synopsis [Performs internal deletion step.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigDelete_int( Abc_Aig_t * pMan )
{
Abc_Obj_t * pNode, * pFanin;
int k;
// get the node to delete
assert( Vec_PtrSize(pMan->vStackDelete) > 0 );
pNode = Vec_PtrPop( pMan->vStackDelete );
// make sure the node is regular and dangling
assert( !Abc_ObjIsComplement(pNode) == 0 );
assert( Abc_ObjFanoutNum(pNode) == 0 );
// skip the constant node
if ( pNode == pMan->pConst1 )
return;
// schedule fanins for deletion if they dangle
Abc_ObjForEachFanin( pNode, pFanin, k )
{
assert( Abc_ObjFanoutNum(pFanin) > 0 );
if ( Abc_ObjFanoutNum(pFanin) == 1 )
Vec_PtrPush( pMan->vStackDelete, pFanin );
}
// remove the node from the table
Abc_AigAndDelete( pMan, pNode );
// remove the node fro the network
Abc_NtkDeleteObj( pNode );
}
/**Function*************************************************************
Synopsis [Returns 1 if the node has at least one complemented fanout.]
@ -298,51 +730,6 @@ bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode )
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_AigResize( Abc_Aig_t * pMan )
{
Abc_Obj_t ** pBinsNew;
Abc_Obj_t * pEnt, * pEnt2;
int nBinsNew, Counter, i, clk;
unsigned Key;
clk = clock();
// get the new table size
nBinsNew = Cudd_PrimeCopy(2 * pMan->nBins);
// allocate a new array
pBinsNew = ALLOC( Abc_Obj_t *, nBinsNew );
memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * nBinsNew );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < pMan->nBins; i++ )
Abc_AigBinForEachEntrySafe( pMan->pBins[i], pEnt, pEnt2 )
{
Key = Abc_HashKey2( Abc_ObjFanin(pEnt,0), Abc_ObjFanin(pEnt,1), nBinsNew );
pEnt->pNext = pBinsNew[Key];
pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
free( pMan->pBins );
pMan->pBins = pBinsNew;
pMan->nBins = nBinsNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

105
src/base/abc/abcCreate.c
View File

@ -32,8 +32,6 @@ static Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
static void Abc_ObjRecycle( Abc_Obj_t * pObj );
static void Abc_ObjAdd( Abc_Obj_t * pObj );
extern void Extra_StopManager( DdManager * dd );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
@ -78,7 +76,9 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type )
else if ( Abc_NtkIsLogicBdd(pNtk) )
pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
else if ( Abc_NtkIsAig(pNtk) )
pNtk->pManFunc = Abc_AigAlloc( pNtk );
pNtk->pManFunc = Abc_AigAlloc( pNtk, 0 );
else if ( Abc_NtkIsSeq(pNtk) )
pNtk->pManFunc = Abc_AigAlloc( pNtk, 1 );
else if ( Abc_NtkIsMapped(pNtk) )
pNtk->pManFunc = Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame());
else
@ -153,6 +153,30 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
}
}
/**Function*************************************************************
Synopsis [Finalizes the network adding latches to CI/CO lists and creates their names.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pLatch;
int i;
// set the COs of the strashed network
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
Vec_PtrPush( pNtk->vCis, pLatch );
Vec_PtrPush( pNtk->vCos, pLatch );
Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") );
}
}
/**Function*************************************************************
Synopsis [Starts a new network using existing network as a model.]
@ -564,16 +588,19 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
{
Abc_Obj_t * pObjNew;
pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
if ( Abc_ObjIsNode(pObj) ) // copy the function
if ( Abc_ObjIsNode(pObj) ) // copy the function if network is the same type
{
if ( Abc_NtkIsSop(pNtkNew) )
pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
else if ( Abc_NtkIsLogicBdd(pNtkNew) )
pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
else if ( Abc_NtkIsMapped(pNtkNew) )
pObjNew->pData = pObj->pData;
else if ( !Abc_NtkIsAig(pNtkNew) )
assert( 0 );
if ( pNtkNew->Type == pObj->pNtk->Type || Abc_NtkIsNetlist(pObj->pNtk) || Abc_NtkIsNetlist(pNtkNew) )
{
if ( Abc_NtkIsSop(pNtkNew) )
pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pObj->pData );
else if ( Abc_NtkIsLogicBdd(pNtkNew) )
pObjNew->pData = Cudd_bddTransfer(pObj->pNtk->pManFunc, pNtkNew->pManFunc, pObj->pData), Cudd_Ref(pObjNew->pData);
else if ( Abc_NtkIsMapped(pNtkNew) )
pObjNew->pData = pObj->pData;
else if ( !Abc_NtkIsAig(pNtkNew) )
assert( 0 );
}
}
else if ( Abc_ObjIsNet(pObj) ) // copy the name
pObjNew->pData = Abc_NtkRegisterName( pNtkNew, pObj->pData );
@ -585,6 +612,55 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
return pObjNew;
}
/**Function*************************************************************
Synopsis [Creates a new constant node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew )
{
Abc_Obj_t * pConst1;
assert( Abc_NtkIsAig(pNtkAig) );
pConst1 = Abc_AigConst1(pNtkAig->pManFunc);
if ( Abc_ObjFanoutNum( pConst1 ) > 0 )
pConst1->pCopy = Abc_NodeCreateConst1( pNtkNew );
return pConst1->pCopy;
}
/**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_NtkIsAig(pNtkAig) );
assert( Abc_NtkIsLogicSop(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_AigConst1(pNtkAig->pManFunc);
Abc_ObjAddFanin( pReset->pCopy, pConst1->pCopy );
}
return pReset->pCopy;
}
/**Function*************************************************************
Synopsis [Deletes the object from the network.]
@ -614,6 +690,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
// remove from the list of objects
Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
pObj->Id = (1<<26)-1;
pNtk->nObjs--;
// perform specialized operations depending on the object type
@ -625,8 +702,8 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
printf( "Error: The net is not in the table...\n" );
assert( 0 );
}
pObj->pData = NULL;
pNtk->nNets--;
assert( !Abc_ObjIsPi(pObj) && !Abc_ObjIsPo(pObj) );
}
else if ( Abc_ObjIsNode(pObj) )
{
@ -898,6 +975,8 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
if ( Abc_NtkIsAig(pNtk) || Abc_NtkIsSeq(pNtk) )
return Abc_AigConst1(pNtk->pManFunc);
pNode = Abc_NtkCreateNode( pNtk );
if ( Abc_NtkIsSop(pNtk) )
pNode->pData = Abc_SopRegister( pNtk->pManFunc, " 1\n" );

28
src/base/abc/abcNetlist.c
View File

@ -230,15 +230,21 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsAig(pNtk) );
// start the network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
// create the constant node
Abc_NtkDupConst1( pNtk, pNtkNew );
// duplicate the nodes and create node functions
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 the choice nodes
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( Abc_NodeIsConst(pObj) )
continue;
if ( !Abc_NodeIsAigChoice(pObj) )
continue;
// create an OR gate
@ -255,12 +261,10 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
// set the new node
pObj->pCopy = pNodeNew;
}
// connect the objects
// connect the objects, including the COs
Abc_NtkForEachObj( pNtk, pObj, i )
Abc_ObjForEachFanin( pObj, pFanin, k )
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
// connect the COs
Abc_NtkFinalize( pNtk, pNtkNew );
// fix the problem with complemented and duplicated CO edges
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// duplicate the EXDC Ntk
@ -299,6 +303,8 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
printf( "Warning: Choice nodes are skipped.\n" );
// start the network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_SOP );
// create the constant node
Abc_NtkDupConst1( pNtk, pNtkNew );
// collect the nodes to be used (marks all nodes with current TravId)
vNodes = Abc_NtkDfs( pNtk );
// create inverters for the CI and remember them
@ -308,8 +314,11 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
// duplicate the nodes, create node functions, and inverters
Vec_PtrForEachEntry( vNodes, pObj, i )
{
Abc_NtkDupObj( pNtkNew, pObj );
pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
if ( !Abc_NodeIsConst(pObj) )
{
Abc_NtkDupObj( pNtkNew, pObj );
pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2 );
}
if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
}
@ -324,7 +333,14 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
}
Vec_PtrFree( vNodes );
// connect the COs
Abc_NtkFinalize( pNtk, pNtkNew );
Abc_NtkForEachCo( pNtk, pObj, i )
{
pFanin = Abc_ObjFanin0(pObj);
if ( Abc_ObjFaninC0( pObj ) )
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
else
Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
}
// fix the problem with complemented and duplicated CO edges
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// duplicate the EXDC Ntk

22
src/base/abc/abcPrint.c
View File

@ -40,11 +40,15 @@
SeeAlso []
***********************************************************************/
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
{
fprintf( pFile, "%-15s:", pNtk->pName );
fprintf( pFile, " i/o = %3d/%3d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
if ( !Abc_NtkIsSeq(pNtk) )
fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
else
fprintf( pFile, " lat = %4d", Abc_NtkSeqLatchNum(pNtk) );
if ( Abc_NtkIsNetlist(pNtk) )
{
@ -56,14 +60,17 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) );
fprintf( pFile, " choice = %5d", Abc_NtkCountChoiceNodes(pNtk) );
}
else if ( Abc_NtkIsSeq(pNtk) )
fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) );
else
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
if ( Abc_NtkIsLogicSop(pNtk) )
{
fprintf( pFile, " cube = %5d", Abc_NtkGetCubeNum(pNtk) );
fprintf( pFile, " lit(sop) = %5d", Abc_NtkGetLitNum(pNtk) );
fprintf( pFile, " lit(fac) = %5d", Abc_NtkGetLitFactNum(pNtk) );
// fprintf( pFile, " lit(sop) = %5d", Abc_NtkGetLitNum(pNtk) );
if ( fFactored )
fprintf( pFile, " lit(fac) = %5d", Abc_NtkGetLitFactNum(pNtk) );
}
else if ( Abc_NtkIsLogicBdd(pNtk) )
fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) );
@ -72,11 +79,14 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
fprintf( pFile, " area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
}
else if ( !Abc_NtkIsAig(pNtk) )
else if ( !Abc_NtkIsAig(pNtk) && !Abc_NtkIsSeq(pNtk) )
{
assert( 0 );
}
fprintf( pFile, " lev = %2d", Abc_NtkGetLevelNum(pNtk) );
if ( !Abc_NtkIsSeq(pNtk) )
fprintf( pFile, " lev = %2d", Abc_NtkGetLevelNum(pNtk) );
fprintf( pFile, "\n" );
}

502
src/base/abc/abcSeq.c Normal file
View File

@ -0,0 +1,502 @@
/**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"
/*
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 reset node.
The reset node producing sequence (01111...) 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.
*/
////////////////////////////////////////////////////////////////////////
/// 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 );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Converts a normal AIG into a sequential AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
assert( Abc_NtkIsAig(pNtk) );
// start the network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_SEQ );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Converts a sequential AIG into a logic SOP network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
{
int fCheck = 1;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj, * pFanin, * pFaninNew;
int i, k;
assert( Abc_NtkIsSeq(pNtk) );
// start the network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_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 ( i = 0; i < Abc_ObjFaninL(pObj, k); i++ )
pFaninNew = pFaninNew->pCopy;
Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
}
// 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 ( fCheck && !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_NtkObjNum(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 )
Abc_NodeSeqCreateLatches( pObj->pCopy, Vec_IntEntry(vNumbers, 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.]
Description [The latches are attached to the node and to each other
through the pCopy field.]
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_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_NtkForEachObj( pNtk, pObj, i )
{
assert( Abc_ObjFanoutLMax(pObj) == Vec_IntEntry(vNumbers, pObj->Id) );
Counter += Vec_IntEntry(vNumbers, pObj->Id);
}
Vec_IntFree( vNumbers );
return Counter;
}
/**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 )
{
Vec_PtrPush( vNodes, pNode );
pNode->fMarkA = 1;
}
// process the nodes
Vec_PtrForEachEntry( vNodes, pNode, i )
{
// 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;
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 )
{
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 ( 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;
assert( Abc_ObjFanoutLMin(pNode) == 0 );
}
}
/**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_ObjFanin0(pFanout) == pObj )
return Abc_ObjFaninL0(pFanout);
else if ( Abc_ObjFanin1(pFanout) == pObj )
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_ObjFanin0(pFanout) == pObj )
Abc_ObjSetFaninL0(pFanout, nLats);
else if ( Abc_ObjFanin1(pFanout) == pObj )
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_ObjFanin0(pFanout) == pObj )
Abc_ObjAddFaninL0(pFanout, nLats);
else if ( Abc_ObjFanin1(pFanout) == pObj )
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 = -1;
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;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

203
src/base/abc/abcSeqRetime.c Normal file
View File

@ -0,0 +1,203 @@
/**CFile****************************************************************
FileName [abcSeqRetime.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Peforms retiming for optimal clock cycle.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcSeqRetime.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// storing arrival times in the nodes
static inline int Abc_NodeReadLValue( Abc_Obj_t * pNode ) { return Vec_IntEntry( (pNode)->pNtk->pData, (pNode)->Id ); }
static inline void Abc_NodeSetLValue( Abc_Obj_t * pNode, int Value ) { Vec_IntWriteEntry( (pNode)->pNtk->pData, (pNode)->Id, (Value) ); }
// the internal procedures
static int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax );
static int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi );
static int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi );
// node status after updating its arrival time
enum { ABC_UPDATE_FAIL, ABC_UPDATE_NO, ABC_UPDATE_YES };
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Retimes AIG for optimal delay.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkSeqRetimeDelay( Abc_Ntk_t * pNtk )
{
int FiMax, FiBest;
assert( Abc_NtkIsSeq( pNtk ) );
// start storage for sequential arrival times
assert( pNtk->pData == NULL );
pNtk->pData = Vec_IntAlloc( 0 );
// get the maximum possible clock
FiMax = Abc_NtkNodeNum(pNtk);
// make sure this clock period is feasible
assert( Abc_NtkRetimeForPeriod( pNtk, FiMax ) );
// search for the optimal clock period between 0 and nLevelMax
FiBest = Abc_NtkRetimeSearch_rec( pNtk, 0, FiMax );
// print the result
printf( "The best clock period is %3d.\n", FiBest );
// free storage
Vec_IntFree( pNtk->pData );
pNtk->pData = NULL;
}
/**Function*************************************************************
Synopsis [Performs binary search for the optimal clock period.]
Description [Assumes that FiMin is infeasible while FiMax is feasible.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkRetimeSearch_rec( Abc_Ntk_t * pNtk, int FiMin, int FiMax )
{
int Median;
assert( FiMin < FiMax );
if ( FiMin + 1 == FiMax )
return FiMax;
Median = FiMin + (FiMax - FiMin)/2;
if ( Abc_NtkRetimeForPeriod( pNtk, Median ) )
return Abc_NtkRetimeSearch_rec( pNtk, FiMin, Median ); // Median is feasible
else
return Abc_NtkRetimeSearch_rec( pNtk, Median, FiMax ); // Median is infeasible
}
/**Function*************************************************************
Synopsis [Returns 1 if retiming with this clock period is feasible.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkRetimeForPeriod( Abc_Ntk_t * pNtk, int Fi )
{
Vec_Ptr_t * vFrontier;
Abc_Obj_t * pObj, * pFanout;
int RetValue, i, k;
// set l-values of all nodes to be minus infinity
Vec_IntFill( pNtk->pData, Abc_NtkObjNum(pNtk), -ABC_INFINITY );
// start the frontier by including PI fanouts
vFrontier = Vec_PtrAlloc( 100 );
Abc_NtkForEachPi( pNtk, pObj, i )
{
Abc_NodeSetLValue( pObj, 0 );
Abc_ObjForEachFanout( pObj, pFanout, k )
if ( pFanout->fMarkA == 0 )
{
Vec_PtrPush( vFrontier, pFanout );
pFanout->fMarkA = 1;
}
}
// iterate until convergence
Vec_PtrForEachEntry( vFrontier, pObj, i )
{
RetValue = Abc_NodeUpdateLValue( pObj, Fi );
if ( RetValue == ABC_UPDATE_FAIL )
break;
// unmark the node as processed
pObj->fMarkA = 0;
if ( RetValue == ABC_UPDATE_NO )
continue;
assert( RetValue == ABC_UPDATE_YES );
// arrival times have changed - add fanouts to the frontier
Abc_ObjForEachFanout( pObj, pFanout, k )
if ( pFanout->fMarkA == 0 )
{
Vec_PtrPush( vFrontier, pFanout );
pFanout->fMarkA = 1;
}
}
// clean the nodes
Vec_PtrForEachEntryStart( vFrontier, pObj, k, i )
pObj->fMarkA = 0;
// report the results
if ( RetValue == ABC_UPDATE_FAIL )
printf( "Period = %3d. Updated nodes = %6d. Infeasible\n", Fi, vFrontier->nSize );
else
printf( "Period = %3d. Updated nodes = %6d. Feasible\n", Fi, vFrontier->nSize );
Vec_PtrFree( vFrontier );
return RetValue != ABC_UPDATE_FAIL;
}
/**Function*************************************************************
Synopsis [Computes the l-value of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NodeUpdateLValue( Abc_Obj_t * pObj, int Fi )
{
int lValueNew, lValue0, lValue1;
assert( !Abc_ObjIsPi(pObj) );
lValue0 = Abc_NodeReadLValue(Abc_ObjFanin0(pObj)) - Fi * Abc_ObjFaninL0(pObj);
if ( Abc_ObjFaninNum(pObj) == 2 )
lValue1 = Abc_NodeReadLValue(Abc_ObjFanin1(pObj)) - Fi * Abc_ObjFaninL1(pObj);
else
lValue1 = -ABC_INFINITY;
lValueNew = 1 + ABC_MAX( lValue0, lValue1 );
if ( Abc_ObjIsPo(pObj) && lValueNew > Fi )
return ABC_UPDATE_FAIL;
if ( lValueNew == Abc_NodeReadLValue(pObj) )
return ABC_UPDATE_NO;
Abc_NodeSetLValue( pObj, lValueNew );
return ABC_UPDATE_YES;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

2
src/base/abc/module.make
View File

@ -22,6 +22,8 @@ SRC += src/base/abc/abc.c \
src/base/abc/abcRenode.c \
src/base/abc/abcRes.c \
src/base/abc/abcSat.c \
src/base/abc/abcSeq.c \
src/base/abc/abcSeqRetime.c \
src/base/abc/abcShow.c \
src/base/abc/abcSop.c \
src/base/abc/abcStrash.c \

3
src/misc/vec/vecPtr.h
View File

@ -51,6 +51,9 @@ struct Vec_Ptr_t_
#define Vec_PtrForEachEntry( vVec, pEntry, i ) \
for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
#define Vec_PtrForEachEntryStart( vVec, pEntry, i, Start ) \
for ( i = Start; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
#define Vec_PtrForEachEntryByLevel( vVec, pEntry, i, k ) \
for ( i = 0; i < Vec_PtrSize(vVec); i++ ) \
Vec_PtrForEachEntry( ((Vec_Ptr_t *)Vec_PtrEntry(vVec, i)), pEntry, k )