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