summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abc.c161
-rw-r--r--src/base/abc/abc.h92
-rw-r--r--src/base/abc/abcAig.c535
-rw-r--r--src/base/abc/abcCreate.c105
-rw-r--r--src/base/abc/abcNetlist.c28
-rw-r--r--src/base/abc/abcPrint.c22
-rw-r--r--src/base/abc/abcSeq.c502
-rw-r--r--src/base/abc/abcSeqRetime.c203
-rw-r--r--src/base/abc/module.make2
-rw-r--r--src/misc/vec/vecPtr.h3
10 files changed, 1518 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 \
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 3914cf99..e7584feb 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -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 )
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 14:49:51 +0000