diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.c | 161 | ||||
-rw-r--r-- | src/base/abc/abc.h | 92 | ||||
-rw-r--r-- | src/base/abc/abcAig.c | 535 | ||||
-rw-r--r-- | src/base/abc/abcCreate.c | 105 | ||||
-rw-r--r-- | src/base/abc/abcNetlist.c | 28 | ||||
-rw-r--r-- | src/base/abc/abcPrint.c | 22 | ||||
-rw-r--r-- | src/base/abc/abcSeq.c | 502 | ||||
-rw-r--r-- | src/base/abc/abcSeqRetime.c | 203 | ||||
-rw-r--r-- | src/base/abc/module.make | 2 |
9 files changed, 1515 insertions, 135 deletions
diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index a02764b1..97d8b56a 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -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************************************************************* diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 99af9ac6..438291d5 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -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 ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 590bc4d2..67f19ba7 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -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,14 +108,38 @@ 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.] Description [] @@ -99,7 +151,13 @@ 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 ); @@ -107,6 +165,90 @@ void Abc_AigFree( Abc_Aig_t * 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.] Description [] @@ -123,6 +265,24 @@ Abc_Obj_t * Abc_AigConst1( Abc_Aig_t * pMan ) /**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.] Description [The argument nodes can be complemented.] @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcCreate.c b/src/base/abc/abcCreate.c index c530f3f6..9412305b 100644 --- a/src/base/abc/abcCreate.c +++ b/src/base/abc/abcCreate.c @@ -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 @@ -155,6 +155,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.] Description [] @@ -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 ); @@ -587,6 +614,55 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ) /**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.] Description [] @@ -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" ); diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 5a4b7447..3f7fae2b 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -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 diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c index 1eac5333..f4833a11 100644 --- a/src/base/abc/abcPrint.c +++ b/src/base/abc/abcPrint.c @@ -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" ); } diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c new file mode 100644 index 00000000..9d4658ce --- /dev/null +++ b/src/base/abc/abcSeq.c @@ -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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcSeqRetime.c b/src/base/abc/abcSeqRetime.c new file mode 100644 index 00000000..ecd8b3d7 --- /dev/null +++ b/src/base/abc/abcSeqRetime.c @@ -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 /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/base/abc/module.make b/src/base/abc/module.make index f698d167..ee494926 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -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 \ |