summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2006-11-02 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2006-11-02 08:01:00 -0800
commitfaf1265bb82f934cc14b6106ccce89e37203efbd (patch)
treef6d69ce4adca5d7e1fdccd3e9848220d6744405d /src/base
parent73bb7932f7edad95086d67a795444537c438309e (diff)
downloadabc-faf1265bb82f934cc14b6106ccce89e37203efbd.tar.gz
abc-faf1265bb82f934cc14b6106ccce89e37203efbd.tar.bz2
abc-faf1265bb82f934cc14b6106ccce89e37203efbd.zip
Version abc61102
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h30
-rw-r--r--src/base/abc/abcCheck.c13
-rw-r--r--src/base/abc/abcDfs.c116
-rw-r--r--src/base/abc/abcFanio.c7
-rw-r--r--src/base/abc/abcLatch.c26
-rw-r--r--src/base/abc/abcNetlist.c13
-rw-r--r--src/base/abc/abcNtk.c71
-rw-r--r--src/base/abc/abcObj.c61
-rw-r--r--src/base/abc/abcRefs.c8
-rw-r--r--src/base/abc/abcShow.c6
-rw-r--r--src/base/abc/abcUtil.c40
-rw-r--r--src/base/abci/abc.c400
-rw-r--r--src/base/abci/abcBmc.c115
-rw-r--r--src/base/abci/abcDsd.c2
-rw-r--r--src/base/abci/abcFpga.c2
-rw-r--r--src/base/abci/abcFpgaFast.c4
-rw-r--r--src/base/abci/abcIvy.c35
-rw-r--r--src/base/abci/abcLut.c4
-rw-r--r--src/base/abci/abcMap.c10
-rw-r--r--src/base/abci/abcNtbdd.c8
-rw-r--r--src/base/abci/abcPrint.c107
-rw-r--r--src/base/abci/abcSweep.c262
-rw-r--r--src/base/abci/abcVerify.c4
-rw-r--r--src/base/abci/abcXsim.c164
-rw-r--r--src/base/abci/module.make4
-rw-r--r--src/base/io/ioUtil.c6
-rw-r--r--src/base/io/ioWriteDot.c13
-rw-r--r--src/base/seq/seqUtil.c3
28 files changed, 1325 insertions, 209 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 149748fc..33345577 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -529,6 +529,8 @@ extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
extern bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
@@ -570,7 +572,8 @@ extern int Abc_NtkLogicToAig( Abc_Ntk_t * pNtk );
extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
extern int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
-/*=== abcLib.c ==========================================================*/
+extern Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+ /*=== abcLib.c ==========================================================*/
extern Abc_Lib_t * Abc_LibCreate( char * pName );
extern void Abc_LibFree( Abc_Lib_t * pLib );
extern Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib );
@@ -595,7 +598,7 @@ extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
-extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
+extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
@@ -604,14 +607,14 @@ extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t * Abc_NodeCreateExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
extern bool Abc_NodeIsConst( Abc_Obj_t * pNode );
extern bool Abc_NodeIsConst0( Abc_Obj_t * pNode );
extern bool Abc_NodeIsConst1( Abc_Obj_t * pNode );
@@ -673,9 +676,11 @@ extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, in
extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
-extern void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll);
+extern void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
+extern void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
/*=== abcProve.c ==========================================================*/
extern int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
+extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
/*=== abcReconv.c ==========================================================*/
extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
extern void Abc_NtkManCutStop( Abc_ManCut_t * p );
@@ -751,7 +756,7 @@ extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
/*=== abcSweep.c ==========================================================*/
extern int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
-extern int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
+extern int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose );
/*=== abcTiming.c ==========================================================*/
extern Abc_Time_t * Abc_NodeReadArrival( Abc_Obj_t * pNode );
extern Abc_Time_t * Abc_NodeReadRequired( Abc_Obj_t * pNode );
@@ -809,6 +814,7 @@ extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
extern Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
extern void Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
+extern int Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
/*=== abcVerify.c ==========================================================*/
extern int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
extern int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 118ea291..d0c1deef 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -167,13 +167,8 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
}
// check the nodes
- if ( Abc_NtkHasAig(pNtk) )
- {
- if ( Abc_NtkIsStrash(pNtk) )
- Abc_AigCheck( pNtk->pManFunc );
- else
- Abc_NtkSeqCheck( pNtk );
- }
+ if ( Abc_NtkIsStrash(pNtk) )
+ Abc_AigCheck( pNtk->pManFunc );
else
{
Abc_NtkForEachNode( pNtk, pNode, i )
@@ -240,9 +235,10 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
Vec_Int_t * vNameIds;
char * pName;
int i, NameId;
-
+/*
if ( Abc_NtkIsNetlist(pNtk) )
{
+
// check that each net has a name
Abc_NtkForEachNet( pNtk, pObj, i )
{
@@ -254,6 +250,7 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
}
}
else
+*/
{
// check that each CI/CO has a name
Abc_NtkForEachCi( pNtk, pObj, i )
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 54676e9d..d9985737 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -209,6 +209,118 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
/**Function*************************************************************
+ Synopsis [Performs DFS for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDfsSeq_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ // if this node is already visited, skip
+ if ( Abc_NodeIsTravIdCurrent( pNode ) )
+ return;
+ // mark the node as visited
+ Abc_NodeSetTravIdCurrent( pNode );
+ // visit the transitive fanin of the node
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ Abc_NtkDfsSeq_rec( pFanin, vNodes );
+ // add the node after the fanins have been added
+ Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes and latches reachable from POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ int i;
+ assert( !Abc_NtkIsNetlist(pNtk) );
+ // set the traversal ID
+ Abc_NtkIncrementTravId( pNtk );
+ // start the array of nodes
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ Abc_NtkDfsSeq_rec( pObj, vNodes );
+ // mark the PIs
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_NtkDfsSeq_rec( pObj, vNodes );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs DFS for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDfsSeqReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+ Abc_Obj_t * pFanout;
+ int i;
+ // if this node is already visited, skip
+ if ( Abc_NodeIsTravIdCurrent( pNode ) )
+ return;
+ // mark the node as visited
+ Abc_NodeSetTravIdCurrent( pNode );
+ // visit the transitive fanin of the node
+ Abc_ObjForEachFanout( pNode, pFanout, i )
+ Abc_NtkDfsSeqReverse_rec( pFanout, vNodes );
+ // add the node after the fanins have been added
+ Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes and latches reachable from POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ int i;
+ assert( !Abc_NtkIsNetlist(pNtk) );
+ // set the traversal ID
+ Abc_NtkIncrementTravId( pNtk );
+ // start the array of nodes
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_NtkDfsSeqReverse_rec( pObj, vNodes );
+ // mark the logic feeding into POs
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ Abc_NtkDfsSeq_rec( pObj, vNodes );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if the ordering of nodes is DFS.]
Description []
@@ -611,9 +723,9 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
Abc_Obj_t * pFanin;
int fAcyclic, i;
assert( !Abc_ObjIsNet(pNode) );
- if ( Abc_ObjIsCi(pNode) || Abc_ObjIsBox(pNode) )
+ if ( Abc_ObjIsCi(pNode) || Abc_ObjIsBox(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsConst(pNode)) )
return 1;
- assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
+ assert( Abc_ObjIsNode(pNode) );
// make sure the node is not visited
assert( !Abc_NodeIsTravIdPrevious(pNode) );
// check if the node is part of the combinational loop
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 8e78ae61..0581b35d 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -223,8 +223,8 @@ void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
int nFanoutsOld, i;
assert( !Abc_ObjIsComplement(pNodeFrom) );
assert( !Abc_ObjIsComplement(pNodeTo) );
- assert( Abc_ObjIsNode(pNodeFrom) );
- assert( Abc_ObjIsNode(pNodeTo) );
+ assert( Abc_ObjIsNode(pNodeFrom) || Abc_ObjIsCi(pNodeFrom) );
+ assert( !Abc_ObjIsPo(pNodeTo) );
assert( pNodeFrom->pNtk == pNodeTo->pNtk );
assert( pNodeFrom != pNodeTo );
assert( Abc_ObjFanoutNum(pNodeFrom) > 0 );
@@ -255,12 +255,9 @@ void Abc_ObjReplace( Abc_Obj_t * pNodeOld, Abc_Obj_t * pNodeNew )
{
assert( !Abc_ObjIsComplement(pNodeOld) );
assert( !Abc_ObjIsComplement(pNodeNew) );
- assert( Abc_ObjIsNode(pNodeOld) );
- assert( Abc_ObjIsNode(pNodeNew) );
assert( pNodeOld->pNtk == pNodeNew->pNtk );
assert( pNodeOld != pNodeNew );
assert( Abc_ObjFanoutNum(pNodeOld) > 0 );
- assert( Abc_ObjFanoutNum(pNodeNew) == 0 );
// transfer the fanouts to the old node
Abc_ObjTransferFanout( pNodeOld, pNodeNew );
// remove the old node
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 8b0a1608..7bc5e264 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -48,7 +48,7 @@ bool Abc_NtkLatchIsSelfFeed_rec( Abc_Obj_t * pLatch, Abc_Obj_t * pLatchRoot )
pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) )
return 0;
- return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch );
+ return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatchRoot );
}
/**Function*************************************************************
@@ -120,7 +120,7 @@ int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk )
if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
pConst1 = Abc_AigConst1(pNtk);
else
- pConst1 = Abc_NodeCreateConst1(pNtk);
+ pConst1 = Abc_NtkCreateNodeConst1(pNtk);
Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pConst1 );
Counter++;
}
@@ -170,6 +170,28 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
}
+/**Function*************************************************************
+
+ Synopsis [Strashes one logic node using its SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vArray;
+ Abc_Obj_t * pLatch;
+ int i;
+ vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ Vec_IntPush( vArray, Abc_LatchIsInit1(pLatch) );
+ return vArray;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index f71093ef..30fab9a3 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -253,9 +253,12 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
}
else if ( Abc_NtkIsSeq(pNtk) )
{
+ assert( 0 );
+/*
pNtkTemp = Abc_NtkSeqToLogicSop(pNtk);
pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
Abc_NtkDelete( pNtkTemp );
+*/
}
else if ( Abc_NtkIsBddLogic(pNtk) )
{
@@ -416,7 +419,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
// if the constant node is used, duplicate it
pObj = Abc_AigConst1(pNtk);
if ( Abc_ObjFanoutNum(pObj) > 0 )
- pObj->pCopy = Abc_NodeCreateConst1(pNtkNew);
+ pObj->pCopy = Abc_NtkCreateNodeConst1(pNtkNew);
// duplicate the nodes and create node functions
Abc_NtkForEachNode( pNtk, pObj, i )
{
@@ -505,19 +508,19 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
pObj = Abc_AigConst1(pNtk);
if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
{
- pObj->pCopy = Abc_NodeCreateConst1(pNtkNew);
- pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+ pObj->pCopy = Abc_NtkCreateNodeConst1(pNtkNew);
+ pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
}
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
- pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+ pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
// duplicate the nodes, create node functions, and inverters
Vec_PtrForEachEntry( vNodes, pObj, i )
{
Abc_NtkDupObj( pNtkNew, pObj, 0 );
pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL );
if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
- pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+ pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
}
// connect the objects
Vec_PtrForEachEntry( vNodes, pObj, i )
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index c99be016..96f489bd 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -69,8 +69,8 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan
// start the functionality manager
if ( Abc_NtkIsStrash(pNtk) )
pNtk->pManFunc = Abc_AigAlloc( pNtk );
- else if ( Abc_NtkIsSeq(pNtk) )
- pNtk->pManFunc = Seq_Create( pNtk );
+// else if ( Abc_NtkIsSeq(pNtk) )
+// pNtk->pManFunc = Seq_Create( pNtk );
else if ( Abc_NtkHasSop(pNtk) )
pNtk->pManFunc = Extra_MmFlexStart();
else if ( Abc_NtkHasBdd(pNtk) )
@@ -301,6 +301,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
printf( "Warning: Structural hashing during duplication reduced %d nodes (this is a minor bug).\n",
Abc_NtkNodeNum(pNtk) - Abc_NtkNodeNum(pNtkNew) );
}
+/*
else if ( Abc_NtkIsSeq(pNtk) )
{
// start the storage for initial states
@@ -333,6 +334,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
Abc_SeqForEachCutsetNode( pNtk, pObj, i )
Vec_PtrPush( pNtkNew->vCutSet, pObj->pCopy );
}
+*/
else
{
// duplicate the nets and nodes (CIs/COs/latches already dupped)
@@ -355,6 +357,65 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Attaches the second network at the bottom of the first.]
+
+ Description [Returns the first network. Deletes the second network.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAttachBottom( Abc_Ntk_t * pNtkTop, Abc_Ntk_t * pNtkBottom )
+{
+ Abc_Obj_t * pObj, * pFanin, * pBuffer;
+ Vec_Ptr_t * vNodes;
+ int i, k;
+ assert( pNtkBottom != NULL );
+ if ( pNtkTop == NULL )
+ return pNtkBottom;
+ // make sure the networks are combinational
+ assert( Abc_NtkPiNum(pNtkTop) == Abc_NtkCiNum(pNtkTop) );
+ assert( Abc_NtkPiNum(pNtkBottom) == Abc_NtkCiNum(pNtkBottom) );
+ // make sure the POs of the bottom correspond to the PIs of the top
+ assert( Abc_NtkPoNum(pNtkBottom) == Abc_NtkPiNum(pNtkTop) );
+ assert( Abc_NtkPiNum(pNtkBottom) < Abc_NtkPiNum(pNtkTop) );
+ // add buffers for the PIs of the top - save results in the POs of the bottom
+ Abc_NtkForEachPi( pNtkTop, pObj, i )
+ {
+ pBuffer = Abc_NtkCreateNodeBuf( pNtkTop, NULL );
+ Abc_ObjTransferFanout( pObj, pBuffer );
+ Abc_NtkPo(pNtkBottom, i)->pCopy = pBuffer;
+ }
+ // remove useless PIs of the top
+ for ( i = Abc_NtkPiNum(pNtkTop) - 1; i >= Abc_NtkPiNum(pNtkBottom); i-- )
+ Abc_NtkDeleteObj( Abc_NtkPi(pNtkTop, i) );
+ assert( Abc_NtkPiNum(pNtkBottom) == Abc_NtkPiNum(pNtkTop) );
+ // copy the bottom network
+ Abc_NtkForEachPi( pNtkBottom, pObj, i )
+ Abc_NtkPi(pNtkBottom, i)->pCopy = Abc_NtkPi(pNtkTop, i);
+ // construct all nodes
+ vNodes = Abc_NtkDfs( pNtkBottom, 0 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ Abc_NtkDupObj(pNtkTop, pObj, 0);
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+ }
+ Vec_PtrFree( vNodes );
+ // connect the POs
+ Abc_NtkForEachPo( pNtkBottom, pObj, i )
+ Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+ // delete old network
+ Abc_NtkDelete( pNtkBottom );
+ // return the network
+ if ( !Abc_NtkCheck( pNtkTop ) )
+ fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" );
+ return pNtkTop;
+}
+
+/**Function*************************************************************
+
Synopsis [Creates the network composed of one logic cone.]
Description []
@@ -720,8 +781,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// start the functionality manager
if ( Abc_NtkIsStrash(pNtk) )
Abc_AigFree( pNtk->pManFunc );
- else if ( Abc_NtkIsSeq(pNtk) )
- Seq_Delete( pNtk->pManFunc );
+// else if ( Abc_NtkIsSeq(pNtk) )
+// Seq_Delete( pNtk->pManFunc );
else if ( Abc_NtkHasSop(pNtk) )
Extra_MmFlexStop( pNtk->pManFunc, 0 );
else if ( Abc_NtkHasBdd(pNtk) )
@@ -777,7 +838,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
if ( Abc_ObjFaninNum(pNet) > 0 )
continue;
// add the constant 0 driver
- pNode = Abc_NodeCreateConst0( pNtk );
+ pNode = Abc_NtkCreateNodeConst0( pNtk );
// add the fanout net
Abc_ObjAddFanin( pNet, pNode );
// add the net to those for which the warning will be printed
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 68bbdb40..ca86565a 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -129,10 +129,10 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
Vec_PtrPush( pNtk->vCos, pObj );
break;
case ABC_OBJ_BI:
- Vec_PtrPush( pNtk->vCis, pObj );
+ if ( pNtk->vCis ) Vec_PtrPush( pNtk->vCis, pObj );
break;
case ABC_OBJ_BO:
- Vec_PtrPush( pNtk->vCos, pObj );
+ if ( pNtk->vCos ) Vec_PtrPush( pNtk->vCos, pObj );
break;
case ABC_OBJ_ASSERT:
Vec_PtrPush( pNtk->vAsserts, pObj );
@@ -146,7 +146,7 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
pObj->pData = (void *)ABC_INIT_NONE;
case ABC_OBJ_TRI:
case ABC_OBJ_BLACKBOX:
- Vec_PtrPush( pNtk->vBoxes, pObj );
+ if ( pNtk->vBoxes ) Vec_PtrPush( pNtk->vBoxes, pObj );
break;
default:
assert(0);
@@ -171,6 +171,9 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
Abc_Ntk_t * pNtk = pObj->pNtk;
Vec_Ptr_t * vNodes;
int i;
+ // remove from the table of names
+ if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
+ Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
// delete fanins and fanouts
assert( !Abc_ObjIsComplement(pObj) );
vNodes = Vec_PtrAlloc( 100 );
@@ -186,9 +189,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
pObj->Id = (1<<26)-1;
pNtk->nObjCounts[pObj->Type]--;
pNtk->nObjs--;
- // remove from the table of names
- if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
- Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
// perform specialized operations depending on the object type
switch (pObj->Type)
{
@@ -210,10 +210,10 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
Vec_PtrRemove( pNtk->vCos, pObj );
break;
case ABC_OBJ_BI:
- Vec_PtrRemove( pNtk->vCis, pObj );
+ if ( pNtk->vCis ) Vec_PtrRemove( pNtk->vCis, pObj );
break;
case ABC_OBJ_BO:
- Vec_PtrRemove( pNtk->vCos, pObj );
+ if ( pNtk->vCos ) Vec_PtrRemove( pNtk->vCos, pObj );
break;
case ABC_OBJ_ASSERT:
Vec_PtrRemove( pNtk->vAsserts, pObj );
@@ -230,7 +230,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
case ABC_OBJ_LATCH:
case ABC_OBJ_TRI:
case ABC_OBJ_BLACKBOX:
- Vec_PtrRemove( pNtk->vBoxes, pObj );
+ if ( pNtk->vBoxes ) Vec_PtrRemove( pNtk->vBoxes, pObj );
break;
default:
assert(0);
@@ -251,20 +251,30 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes )
{
Abc_Ntk_t * pNtk = pObj->pNtk;
Vec_Ptr_t * vNodes;
int i;
assert( !Abc_ObjIsComplement(pObj) );
+ assert( !Abc_ObjIsPi(pObj) );
assert( Abc_ObjFanoutNum(pObj) == 0 );
// delete fanins and fanouts
vNodes = Vec_PtrAlloc( 100 );
Abc_NodeCollectFanins( pObj, vNodes );
Abc_NtkDeleteObj( pObj );
- Vec_PtrForEachEntry( vNodes, pObj, i )
- if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
- Abc_NtkDeleteObj_rec( pObj );
+ if ( fOnlyNodes )
+ {
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+ Abc_NtkDeleteObj_rec( pObj, fOnlyNodes );
+ }
+ else
+ {
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ if ( !Abc_ObjIsPi(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+ Abc_NtkDeleteObj_rec( pObj, fOnlyNodes );
+ }
Vec_PtrFree( vNodes );
}
@@ -530,7 +540,7 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
+Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
@@ -559,7 +569,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
+Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pNode;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
@@ -588,12 +598,12 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
+Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
{
Abc_Obj_t * pNode;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
pNode = Abc_NtkCreateNode( pNtk );
- Abc_ObjAddFanin( pNode, pFanin );
+ if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
if ( Abc_NtkHasSop(pNtk) )
pNode->pData = Abc_SopRegister( pNtk->pManFunc, "0 1\n" );
else if ( Abc_NtkHasBdd(pNtk) )
@@ -618,12 +628,12 @@ Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
+Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
{
Abc_Obj_t * pNode;
assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
- pNode = Abc_NtkCreateNode( pNtk );
- Abc_ObjAddFanin( pNode, pFanin );
+ pNode = Abc_NtkCreateNode( pNtk );
+ if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
if ( Abc_NtkHasSop(pNtk) )
pNode->pData = Abc_SopRegister( pNtk->pManFunc, "1 1\n" );
else if ( Abc_NtkHasBdd(pNtk) )
@@ -648,7 +658,7 @@ Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
+Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
{
Abc_Obj_t * pNode;
int i;
@@ -678,7 +688,7 @@ Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
+Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
{
Abc_Obj_t * pNode;
int i;
@@ -708,7 +718,7 @@ Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
+Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
{
Abc_Obj_t * pNode;
int i;
@@ -738,7 +748,7 @@ Abc_Obj_t * Abc_NodeCreateExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 )
+Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 )
{
Abc_Obj_t * pNode;
assert( Abc_NtkIsLogic(pNtk) );
@@ -772,8 +782,7 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
bool Abc_NodeIsConst( Abc_Obj_t * pNode )
{
assert( Abc_NtkIsLogic(pNode->pNtk) || Abc_NtkIsNetlist(pNode->pNtk) );
- assert( Abc_ObjIsNode(pNode) );
- return Abc_ObjFaninNum(pNode) == 0;
+ return Abc_ObjIsNode(pNode) && Abc_ObjFaninNum(pNode) == 0;
}
/**Function*************************************************************
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index ea076e47..bc9c316f 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -316,12 +316,18 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu
void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode )
{
Vec_Ptr_t * vCone, * vSupp;
+ Abc_Obj_t * pObj;
+ int i;
vCone = Vec_PtrAlloc( 100 );
vSupp = Vec_PtrAlloc( 100 );
Abc_NodeDeref_rec( pNode );
Abc_NodeMffsConeSupp( pNode, vCone, vSupp );
Abc_NodeRef_rec( pNode );
- printf( "Cone = %6d. Supp = %6d. \n", Vec_PtrSize(vCone), Vec_PtrSize(vSupp) );
+ printf( "Node = %6s : Supp = %3d Cone = %3d (",
+ Abc_ObjName(pNode), Vec_PtrSize(vSupp), Vec_PtrSize(vCone) );
+ Vec_PtrForEachEntry( vCone, pObj, i )
+ printf( " %s", Abc_ObjName(pObj) );
+ printf( " )\n" );
Vec_PtrFree( vCone );
Vec_PtrFree( vSupp );
}
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index bb0606f7..8ed653a9 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -88,7 +88,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
-void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
+void Abc_NtkShowAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesShow )
{
FILE * pFile;
Abc_Obj_t * pNode;
@@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
char FileNameDot[200];
int i;
- assert( Abc_NtkHasAig(pNtk) );
+ assert( Abc_NtkIsStrash(pNtk) );
// create the file name
Abc_ShowGetFileName( pNtk->pName, FileNameDot );
// check that the file can be opened
@@ -112,7 +112,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
Abc_NtkForEachObj( pNtk, pNode, i )
Vec_PtrPush( vNodes, pNode );
// write the DOT file
- Io_WriteDotAig( pNtk, vNodes, NULL, FileNameDot, 0 );
+ Io_WriteDotAig( pNtk, vNodes, vNodesShow, FileNameDot, 0 );
Vec_PtrFree( vNodes );
// visualize the file
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 6e506b0e..d5a4b5cb 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -81,6 +81,17 @@ void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk )
Vec_PtrPush( pNtk->vCos, pObj );
Abc_NtkForEachBox( pNtk, pObj, i )
{
+ if ( Abc_ObjIsLatch(pObj) )
+ continue;
+ Abc_ObjForEachFanin( pObj, pTerm, k )
+ Vec_PtrPush( pNtk->vCos, pTerm );
+ Abc_ObjForEachFanout( pObj, pTerm, k )
+ Vec_PtrPush( pNtk->vCis, pTerm );
+ }
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ {
+ if ( !Abc_ObjIsLatch(pObj) )
+ continue;
Abc_ObjForEachFanin( pObj, pTerm, k )
Vec_PtrPush( pNtk->vCos, pTerm );
Abc_ObjForEachFanout( pObj, pTerm, k )
@@ -545,11 +556,11 @@ void Abc_NtkFixCoDriverProblem( Abc_Obj_t * pDriver, Abc_Obj_t * pNodeCo, int fD
// add inverters and buffers when necessary
if ( Abc_ObjFaninC0(pNodeCo) )
{
- pDriverNew = Abc_NodeCreateInv( pNtk, pDriver );
+ pDriverNew = Abc_NtkCreateNodeInv( pNtk, pDriver );
Abc_ObjXorFaninC( pNodeCo, 0 );
}
else
- pDriverNew = Abc_NodeCreateBuf( pNtk, pDriver );
+ pDriverNew = Abc_NtkCreateNodeBuf( pNtk, pDriver );
}
// update the fanin of the PO node
Abc_ObjPatchFanin( pNodeCo, pDriver, pDriverNew );
@@ -925,13 +936,14 @@ int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
}
else
fclose( pFile );
-
+/*
if ( Abc_NtkIsSeq(pNtk) )
{
pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
*pfDelete1 = 1;
}
else
+*/
pNtk1 = pNtk;
pNtk2 = Io_Read( pNtk->pSpec, fCheck );
if ( pNtk2 == NULL )
@@ -945,12 +957,14 @@ int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
fprintf( pErr, "Empty current network.\n" );
return 0;
}
+/*
if ( Abc_NtkIsSeq(pNtk) )
{
pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
*pfDelete1 = 1;
}
else
+*/
pNtk1 = pNtk;
pNtk2 = Io_Read( argv[util_optind], fCheck );
if ( pNtk2 == NULL )
@@ -1265,6 +1279,26 @@ void Abc_NtkDetectMatching( Abc_Ntk_t * pNtk )
}
+/**Function*************************************************************
+
+ Synopsis [Compares the pointers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_ObjPointerCompare( void ** pp1, void ** pp2 )
+{
+ if ( *pp1 < *pp2 )
+ return -1;
+ if ( *pp1 > *pp2 )
+ return 1;
+ return 0;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b25ca2f7..5d6af56d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36,6 +36,7 @@ static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -90,6 +91,7 @@ static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -102,6 +104,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -166,6 +169,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_io", Abc_CommandPrintIo, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_latch", Abc_CommandPrintLatch, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_fanio", Abc_CommandPrintFanio, 0 );
+ Cmd_CommandAdd( pAbc, "Printing", "print_mffc", Abc_CommandPrintMffc, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
@@ -220,6 +224,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 );
Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 );
Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "xsim", Abc_CommandXsim, 0 );
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 );
@@ -232,6 +237,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "bmc", Abc_CommandBmc, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 );
@@ -250,15 +256,15 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga", Abc_CommandFpgaFast, 1 );
Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 );
- Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 );
+// Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
- Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
+// Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
@@ -269,8 +275,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 );
// Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 );
- Cmd_CommandAdd( pAbc, "Sequential", "howard", Abc_CommandHoward, 0 );
- Cmd_CommandAdd( pAbc, "Sequential", "skew_fwd", Abc_CommandSkewForward, 0 );
+// Cmd_CommandAdd( pAbc, "Sequential", "howard", Abc_CommandHoward, 0 );
+// Cmd_CommandAdd( pAbc, "Sequential", "skew_fwd", Abc_CommandSkewForward, 0 );
// Rwt_Man4ExploreStart();
// Map_Var3Print();
@@ -629,6 +635,58 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandPrintMffc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ extern void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ // print the nodes
+ Abc_NtkPrintMffc( pOut, pNtk );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: print_mffc [-h]\n" );
+ fprintf( pErr, "\t prints the MFFC of each node in the network\n" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -1581,7 +1639,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
int c;
int fMulti;
- extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk );
+ extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesShow );
extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -1609,7 +1667,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( !Abc_NtkHasAig(pNtk) )
+ if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Visualizing networks other than AIGs can be done using command \"show_ntk\".\n" );
return 1;
@@ -1622,7 +1680,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !fMulti )
- Abc_NtkShowAig( pNtk );
+ Abc_NtkShowAig( pNtk, NULL );
else
Abc_NtkShowMulti( pNtk );
return 0;
@@ -1683,7 +1741,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkHasAig(pNtk) )
+ if ( Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Visualizing AIG can only be done using command \"show_aig\".\n" );
return 1;
@@ -4975,14 +5033,97 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nFrames;
+ int fInputs;
+ int fVerbose;
+ extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 10;
+ fInputs = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
+ case 'i':
+ fInputs ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Only works for strashed networks.\n" );
+ return 1;
+ }
+
+ Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
+ fprintf( pErr, "\t performs X-valued simulation of the AIG\n" );
+ fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
+ fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes;
+ Abc_Ntk_t * pNtk;//, * pNtkRes;
int c;
int nLevels;
// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
- extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
+// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
+ extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -5064,7 +5205,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Ivy_TruthEstimateNodesTest();
-
+/*
pNtkRes = Abc_NtkIvy( pNtk );
// pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 );
// pNtkRes = NULL;
@@ -5075,7 +5216,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-
+*/
+ Abc_NtkMaxFlowTest( pNtk );
return 0;
usage:
@@ -5100,7 +5242,7 @@ usage:
int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes;
+ Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
int c;
extern Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk );
@@ -5132,11 +5274,12 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkIsStrash(pNtk) )
{
- fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" );
- return 1;
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
+ pNtkRes = Abc_NtkIvyStrash( pNtkTemp );
+ Abc_NtkDelete( pNtkTemp );
}
-
- pNtkRes = Abc_NtkIvyStrash( pNtk );
+ else
+ pNtkRes = Abc_NtkIvyStrash( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5741,9 +5884,9 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nIters = 3;
- fUseZeroCost = 1;
- fVerbose = 0;
+ nIters = 2;
+ fUseZeroCost = 0;
+ fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF )
{
@@ -5869,6 +6012,94 @@ usage:
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nFrames;
+ int fInit;
+ int fVerbose;
+
+ extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 5;
+ fInit = 0;
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
+ case 'i':
+ fInit ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 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, "Only works for non-sequential networks.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsStrash(pNtk) )
+ Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
+ else
+ {
+ pNtk = Abc_NtkStrash( pNtk, 0, 1 );
+ Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
+ Abc_NtkDelete( pNtk );
+ }
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: bmc [-K num] [-ivh]\n" );
+ fprintf( pErr, "\t perform bounded model checking\n" );
+ fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-i : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
/**Function*************************************************************
@@ -7573,48 +7804,38 @@ usage:
int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp;
+ Abc_Ntk_t * pNtk, * pNtkTemp;
int c, nMaxIters;
- int fForward;
- int fBackward;
int fInitial;
int fVerbose;
+ int Mode;
+ extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fForward = 0;
- fBackward = 0;
+ Mode = 3;
fInitial = 1;
- fVerbose = 0;
+ fVerbose = 1;
nMaxIters = 15;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Ifbivh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF )
{
switch ( c )
{
- case 'I':
+ case 'M':
if ( globalUtilOptind >= argc )
{
- fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" );
+ fprintf( pErr, "Command line switch \"-M\" should be followed by a positive integer.\n" );
goto usage;
}
- nMaxIters = atoi(argv[globalUtilOptind]);
+ Mode = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nMaxIters < 0 )
+ if ( Mode < 0 )
goto usage;
break;
- case 'f':
- fForward ^= 1;
- break;
- case 'b':
- fBackward ^= 1;
- break;
- case 'i':
- fInitial ^= 1;
- break;
case 'v':
fVerbose ^= 1;
break;
@@ -7631,61 +7852,56 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 )
+ if ( !Abc_NtkLatchNum(pNtk) )
{
fprintf( pErr, "The network has no latches. Retiming is not performed.\n" );
return 0;
}
- if ( Abc_NtkHasAig(pNtk) )
+ if ( Abc_NtkIsStrash(pNtk) )
{
- // quit if there are choice nodes
if ( Abc_NtkGetChoiceNum(pNtk) )
{
- fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" );
+ fprintf( pErr, "Retiming with choice nodes is not implemented.\n" );
return 0;
}
- if ( Abc_NtkIsStrash(pNtk) )
- pNtkRes = Abc_NtkAigToSeq(pNtk);
- else
- pNtkRes = Abc_NtkDup(pNtk);
- // retime the network
- if ( fForward )
- Seq_NtkSeqRetimeForward( pNtkRes, fInitial, fVerbose );
- else if ( fBackward )
- Seq_NtkSeqRetimeBackward( pNtkRes, fInitial, fVerbose );
- else
- Seq_NtkSeqRetimeDelay( pNtkRes, nMaxIters, fInitial, fVerbose );
- // if the network is an AIG, convert the result into an AIG
- if ( Abc_NtkIsStrash(pNtk) )
- {
- pNtkRes = Abc_NtkSeqToLogicSop( pNtkTemp = pNtkRes );
- Abc_NtkDelete( pNtkTemp );
- pNtkRes = Abc_NtkStrash( pNtkTemp = pNtkRes, 0, 0 );
- Abc_NtkDelete( pNtkTemp );
- }
+ pNtk = Abc_NtkAigToLogicSop( pNtkTemp = pNtk );
+ Abc_NtkDelete( pNtkTemp );
}
- else
- pNtkRes = Seq_NtkRetime( pNtk, nMaxIters, fInitial, fVerbose );
- // replace the network
- if ( pNtkRes == NULL )
+
+ // get the network in the SOP form
+ if ( !Abc_NtkLogicToSop(pNtk, 0) )
{
- fprintf( pErr, "Retiming has failed.\n" );
+ printf( "Converting to SOPs has failed.\n" );
return 0;
}
- // replace the current network
- Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "The network is not a logic network. Retiming is not performed.\n" );
+ return 0;
+ }
+
+ // perform the retiming
+ Abc_NtkRetime( pNtk, Mode, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: retime [-I num] [-fbih]\n" );
- fprintf( pErr, "\t retimes the current network using Pan's delay-optimal retiming\n" );
- fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
- fprintf( pErr, "\t-f : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" );
- fprintf( pErr, "\t-b : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" );
- fprintf( pErr, "\t-i : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" );
+ fprintf( pErr, "usage: retime [-M num] [-vh]\n" );
+ fprintf( pErr, "\t retimes the current network using one of the algorithms:\n" );
+ fprintf( pErr, "\t 1: most forward retiming\n" );
+ fprintf( pErr, "\t 2: most backward retiming\n" );
+ fprintf( pErr, "\t 3: min-area retiming\n" );
+ fprintf( pErr, "\t 4: min-delay retiming\n" );
+ fprintf( pErr, "\t 5: min-area under min-delay constraint retiming\n" );
+ fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
+// fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters );
+// fprintf( pErr, "\t-f : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" );
+// fprintf( pErr, "\t-b : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" );
+// fprintf( pErr, "\t-i : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" );
}
/**Function*************************************************************
@@ -8069,17 +8285,22 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
+ int fVerbose;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fVerbose = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -8091,18 +8312,23 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( !Abc_NtkIsSeq(pNtk) )
+ if ( !Abc_NtkIsLogic(pNtk) )
{
- fprintf( pErr, "Only works for sequential AIGs.\n" );
+ fprintf( pErr, "Only works for logic networks.\n" );
return 1;
}
// modify the current network
- Seq_NtkCleanup( pNtk, 1 );
+ Abc_NtkCleanupSeq( pNtk, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: scleanup [-h]\n" );
+ fprintf( pErr, "usage: scleanup [-vh]\n" );
fprintf( pErr, "\t performs sequential cleanup\n" );
+ fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" );
+ fprintf( pErr, "\t - removes and shared latches driven by constants\n" );
+ fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" );
+ fprintf( pErr, "\t (the latter may change sequential behaviour)\n" );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c
new file mode 100644
index 00000000..af6d237b
--- /dev/null
+++ b/src/base/abci/abcBmc.c
@@ -0,0 +1,115 @@
+/**CFile****************************************************************
+
+ FileName [abcBmc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Performs bounded model check.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
+
+static void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose )
+{
+ Ivy_FraigParams_t Params, * pParams = &Params;
+ Ivy_Man_t * pMan, * pFrames, * pFraig;
+ Vec_Ptr_t * vMapping;
+ // convert to IVY manager
+ pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+ // generate timeframes
+ pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping );
+ // fraig the timeframes
+ Ivy_FraigParamsDefault( pParams );
+ pParams->nBTLimitNode = ABC_INFINITY;
+ pParams->fVerbose = 0;
+ pParams->fProve = 0;
+ pFraig = Ivy_FraigPerform( pFrames, pParams );
+printf( "Frames have %6d nodes. ", Ivy_ManNodeNum(pFrames) );
+printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
+ // report the classes
+// if ( fVerbose )
+// Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
+ // free stuff
+ Vec_PtrFree( vMapping );
+ Ivy_ManStop( pFraig );
+ Ivy_ManStop( pFrames );
+ Ivy_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames )
+{
+ Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3;
+ int i, f, nIdMax, Prev2, Prev3;
+ nIdMax = Ivy_ManObjIdMax(pMan);
+ // check what is the number of nodes in each frame
+ Prev2 = Prev3 = 0;
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Ivy_ManForEachNode( pMan, pFirst1, i )
+ {
+ pFirst2 = Ivy_Regular( Vec_PtrEntry(vMapping, f * nIdMax + pFirst1->Id) );
+ if ( Ivy_ObjIsConst1(pFirst2) || pFirst2->Type == 0 )
+ continue;
+ pFirst3 = Ivy_Regular( pFirst2->pEquiv );
+ if ( Ivy_ObjIsConst1(pFirst3) || pFirst3->Type == 0 )
+ continue;
+ break;
+ }
+ if ( f )
+ printf( "Frame %3d : Strash = %5d Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 );
+ Prev2 = pFirst2->Id;
+ Prev3 = pFirst3->Id;
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 6708217c..b38012cd 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
int i, nNodesDsd;
// save the CI nodes in the DSD nodes
- Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) );
+ Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index 80238b48..3bc9fbed 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -210,7 +210,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy );
// set the constant node
// if ( Fpga_NodeReadRefs(Fpga_ManReadConst1(pMan)) > 0 )
- Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) );
+ Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NtkCreateNodeConst1(pNtkNew) );
// process the nodes in topological order
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c
index b307273f..3ad29291 100644
--- a/src/base/abci/abcFpgaFast.c
+++ b/src/base/abci/abcFpgaFast.c
@@ -99,7 +99,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
// start the new ABC network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
// transfer the pointers to the basic nodes
- Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) );
+ Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkCreateNodeConst1(pNtkNew) );
Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc );
// recursively construct the network
@@ -112,7 +112,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
{
if ( Abc_ObjIsCi(pObjAbc) )
- pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc );
+ pObjAbc = Abc_NtkCreateNodeInv( pNtkNew, pObjAbc );
else
{
// clone the node
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 82e03119..446eb0cc 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -51,7 +51,7 @@ static inline Abc_Obj_t * Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge ) {
static inline Abc_Obj_t * Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
static inline Abc_Obj_t * Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
-static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs );
+static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -85,7 +85,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
{
printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
- return NULL;
+// return NULL;
}
// print warning about choice nodes
if ( Abc_NtkGetChoiceNum( pNtk ) )
@@ -102,9 +102,9 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
if ( fSeq )
{
int nLatches = Abc_NtkLatchNum(pNtk);
- int * pInit = Abc_NtkCollectLatchValues( pNtk, fUseDc );
- Ivy_ManMakeSeq( pMan, nLatches, pInit );
- FREE( pInit );
+ Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
+ Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
+ Vec_IntFree( vInit );
// Ivy_ManPrintStats( pMan );
}
return pMan;
@@ -191,8 +191,8 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
return NULL;
Ivy_ManHaigStart( pMan, fVerbose );
- Ivy_ManRewriteSeq( pMan, 0, 0 );
- for ( i = 1; i < nIters; i++ )
+// Ivy_ManRewriteSeq( pMan, 0, 0 );
+ for ( i = 0; i < nIters; i++ )
Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
Ivy_ManHaigPostprocess( pMan, fVerbose );
@@ -486,7 +486,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
int fCleanup = 1;
// int nNodes;
int nLatches = Abc_NtkLatchNum(pNtk);
- int * pInit = Abc_NtkCollectLatchValues( pNtk, 0 );
+ Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
assert( !Abc_NtkIsNetlist(pNtk) );
assert( !Abc_NtkIsSeq(pNtk) );
@@ -494,7 +494,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
{
- FREE( pInit );
+ Vec_IntFree( vInit );
printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
return NULL;
}
@@ -513,7 +513,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
pMan = Abc_NtkToAig( pNtk );
if ( !Ivy_ManCheck( pMan ) )
{
- FREE( pInit );
+ Vec_IntFree( vInit );
printf( "AIG check has failed.\n" );
Ivy_ManStop( pMan );
return NULL;
@@ -975,22 +975,23 @@ Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, cha
SeeAlso []
***********************************************************************/
-int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs )
+Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
{
Abc_Obj_t * pLatch;
- int * pArray, i;
- pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+ Vec_Int_t * vArray;
+ int i;
+ vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i )
{
if ( fUseDcs || Abc_LatchIsInitDc(pLatch) )
- pArray[i] = IVY_INIT_DC;
+ Vec_IntPush( vArray, IVY_INIT_DC );
else if ( Abc_LatchIsInit1(pLatch) )
- pArray[i] = IVY_INIT_1;
+ Vec_IntPush( vArray, IVY_INIT_1 );
else if ( Abc_LatchIsInit0(pLatch) )
- pArray[i] = IVY_INIT_0;
+ Vec_IntPush( vArray, IVY_INIT_0 );
else assert( 0 );
}
- return pArray;
+ return vArray;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index 165d84c5..61b1ce78 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -148,7 +148,7 @@ int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int
// if there is no delay improvement, skip; otherwise, update level
if ( pObjTop->Level >= pObj->Level )
{
- Abc_NtkDeleteObj_rec( pObjTop );
+ Abc_NtkDeleteObj_rec( pObjTop, 1 );
continue;
}
pObj->Level = pObjTop->Level;
@@ -570,7 +570,7 @@ Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
{
Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
- Abc_NtkDeleteObj_rec( pFanin );
+ Abc_NtkDeleteObj_rec( pFanin, 1 );
return NULL;
}
// create the topmost node
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 276e41d0..c4f9850a 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -259,7 +259,7 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int
// check the case of constant node
if ( Map_NodeIsConst(pNodeMap) )
- return fPhase? Abc_NodeCreateConst1(pNtkNew) : Abc_NodeCreateConst0(pNtkNew);
+ return fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
// check if the phase is already implemented
pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase );
@@ -369,7 +369,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap
* (since the cut only has 4 variables). An interesting question is what
* if the first variable (and not the fifth one is the redundant one;
* can that happen?) */
- return Abc_NodeCreateConst0(pNtkNew);
+ return Abc_NtkCreateNodeConst0(pNtkNew);
}
}
@@ -503,14 +503,14 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
// set the pointers from the mapper to the new nodes
Abc_NtkForEachCi( pNtk, pNode, i )
{
- Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+ Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) );
Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy );
}
Abc_NtkForEachNode( pNtk, pNode, i )
{
// if ( Abc_NodeIsConst(pNode) )
// continue;
- Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+ Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) );
Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy );
}
@@ -630,7 +630,7 @@ Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * p
* (since the cut only has 4 variables). An interesting question is what
* if the first variable (and not the fifth one is the redundant one;
* can that happen?) */
- return Abc_NodeCreateConst0(pNtkNew);
+ return Abc_NtkCreateNodeConst0(pNtkNew);
}
}
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 9b67ab13..a1f6b9f9 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -195,7 +195,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
st_free_table( tBdd2Node );
if ( Cudd_IsComplement(bFunc) )
- pNodeNew = Abc_NodeCreateInv( pNtkNew, pNodeNew );
+ pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
return pNodeNew;
}
@@ -215,18 +215,18 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
assert( !Cudd_IsComplement(bFunc) );
if ( bFunc == b1 )
- return Abc_NodeCreateConst1(pNtkNew);
+ return Abc_NtkCreateNodeConst1(pNtkNew);
if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
return pNodeNew;
// solve for the children nodes
pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
if ( Cudd_IsComplement(cuddE(bFunc)) )
- pNodeNew0 = Abc_NodeCreateInv( pNtkNew, pNodeNew0 );
+ pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
assert( 0 );
// create the MUX node
- pNodeNew = Abc_NodeCreateMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
+ pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
return pNodeNew;
}
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index afc635e9..6af12afd 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -61,10 +61,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
else
fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
- if ( !Abc_NtkIsSeq(pNtk) )
+// if ( !Abc_NtkIsSeq(pNtk) )
fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
- else
- fprintf( pFile, " lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
+// else
+// fprintf( pFile, " lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
if ( Abc_NtkIsNetlist(pNtk) )
{
@@ -228,6 +228,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
int InitNums[4], Init;
assert( !Abc_NtkIsNetlist(pNtk) );
+/*
if ( Abc_NtkIsSeq(pNtk) )
{
Seq_NtkLatchGetInitNums( pNtk, InitNums );
@@ -236,7 +237,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
return;
}
-
+*/
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
fprintf( pFile, "The network is combinational.\n" );
@@ -383,6 +384,26 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode )
/**Function*************************************************************
+ Synopsis [Prints the MFFCs of the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int i;
+ extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ Abc_NodeMffsConeSuppPrint( pNode );
+}
+
+/**Function*************************************************************
+
Synopsis [Prints the factored form of one node.]
Description []
@@ -833,6 +854,84 @@ void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ) {
fprintf( pFile, "Endpoint Skews : Total |Skew| = %.2f\t Avg |Skew| = %.2f\t Non-Zero Skews = %d\n",
sum, avg, nNonZero );
}
+
+/**Function*************************************************************
+
+ Synopsis [Prints information about the object.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ fprintf( pFile, "Object %5d : ", pObj->Id );
+ switch ( pObj->Type )
+ {
+ case ABC_OBJ_NONE:
+ fprintf( pFile, "NONE " );
+ break;
+ case ABC_OBJ_CONST1:
+ fprintf( pFile, "Const1 " );
+ break;
+ case ABC_OBJ_PIO:
+ fprintf( pFile, "PIO " );
+ break;
+ case ABC_OBJ_PI:
+ fprintf( pFile, "PI " );
+ break;
+ case ABC_OBJ_PO:
+ fprintf( pFile, "PO " );
+ break;
+ case ABC_OBJ_BI:
+ fprintf( pFile, "BI " );
+ break;
+ case ABC_OBJ_BO:
+ fprintf( pFile, "BO " );
+ break;
+ case ABC_OBJ_ASSERT:
+ fprintf( pFile, "Assert " );
+ break;
+ case ABC_OBJ_NET:
+ fprintf( pFile, "Net " );
+ break;
+ case ABC_OBJ_NODE:
+ fprintf( pFile, "Node " );
+ break;
+ case ABC_OBJ_GATE:
+ fprintf( pFile, "Gate " );
+ break;
+ case ABC_OBJ_LATCH:
+ fprintf( pFile, "Latch " );
+ break;
+ case ABC_OBJ_TRI:
+ fprintf( pFile, "Tristate" );
+ break;
+ case ABC_OBJ_BLACKBOX:
+ fprintf( pFile, "Blackbox" );
+ break;
+ default:
+ assert(0);
+ break;
+ }
+ // print the fanins
+ fprintf( pFile, " Fanins ( " );
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ fprintf( pFile, "%d ", pFanin->Id );
+ fprintf( pFile, ") " );
+ // print the logic function
+ if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) )
+ fprintf( pFile, " %s", pObj->pData );
+ else
+ fprintf( pFile, "\n" );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index cac634da..076bee46 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -32,6 +32,7 @@ static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t
static void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
static int Abc_NodeDroppingCost( Abc_Obj_t * pNode );
+static int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
static void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
static void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 );
static void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin );
@@ -425,7 +426,7 @@ void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv,
return;
// add the invertor
- pNodeMinInv = Abc_NodeCreateInv( pNtk, pNodeMin );
+ pNodeMinInv = Abc_NtkCreateNodeInv( pNtk, pNodeMin );
// move the fanouts of the inverted nodes
for ( pNode = pListInv; pNode; pNode = pNode->pNext )
@@ -583,7 +584,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
if ( Abc_ObjFanoutNum(pNode) > 0 )
Vec_PtrPush( vNodes, pNode );
else
- Abc_NtkDeleteObj_rec( pNode );
+ Abc_NtkDeleteObj_rec( pNode, 1 );
}
Vec_PtrFree( vNodes );
// sweep a node into its CO fanout if all of this is true:
@@ -672,6 +673,263 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
Cudd_RecursiveDeref( dd, bCof1 );
}
+
+
+/**Function*************************************************************
+
+ Synopsis [Removes all objects whose trav ID is not current.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeRemoveNonCurrentObjects( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj;
+ int Counter, i;
+ int fVerbose = 0;
+
+ // report on the nodes to be deleted
+ if ( fVerbose )
+ {
+ printf( "These nodes will be deleted: \n" );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( !Abc_NodeIsTravIdCurrent( pObj ) )
+ {
+ printf( " " );
+ Abc_ObjPrint( stdout, pObj );
+ }
+ }
+
+ // delete the nodes
+ Counter = 0;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( !Abc_NodeIsTravIdCurrent( pObj ) )
+ {
+ Abc_NtkDeleteObj( pObj );
+ Counter++;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the fanin of this latch is a constant.]
+
+ Description [Returns 0/1 if constant; -1 if not a constant.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSetTravId_rec( Abc_Obj_t * pObj )
+{
+ Abc_NodeSetTravIdCurrent(pObj);
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ return;
+ assert( Abc_ObjFaninNum(pObj) == 1 );
+ Abc_NtkSetTravId_rec( Abc_ObjFanin0(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the fanin of this latch is a constant.]
+
+ Description [Returns 0/1 if constant; -1 if not a constant.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkCheckConstant_rec( Abc_Obj_t * pObj )
+{
+ if ( Abc_ObjFaninNum(pObj) == 0 )
+ {
+ if ( !Abc_ObjIsNode(pObj) )
+ return -1;
+ if ( Abc_NodeIsConst0(pObj) )
+ return 0;
+ if ( Abc_NodeIsConst1(pObj) )
+ return 1;
+ assert( 0 );
+ return -1;
+ }
+ if ( Abc_ObjIsLatch(pObj) || Abc_ObjFaninNum(pObj) > 1 )
+ return -1;
+ if ( !Abc_ObjIsNode(pObj) || Abc_NodeIsBuf(pObj) )
+ return Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) );
+ if ( Abc_NodeIsInv(pObj) )
+ {
+ int RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) );
+ if ( RetValue == 0 )
+ return 1;
+ if ( RetValue == 1 )
+ return 0;
+ return RetValue;
+ }
+ assert( 0 );
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes redundant latches.]
+
+ Description [The redundant latches are of two types:
+ - Latches fed by a constant which matches the init value of the latch.
+ - Latches fed by a constant which does not match the init value of the latch
+ can be all replaced by one latch.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkLatchSweep( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pFanin, * pLatch, * pLatchPivot = NULL;
+ int Counter, RetValue, i;
+ Counter = 0;
+ // go through the latches
+ Abc_NtkForEachLatch( pNtk, pLatch, i )
+ {
+ // check if the latch has constant input
+ RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pLatch) );
+ if ( RetValue == -1 )
+ continue;
+ // found a latch with constant fanin
+ if ( (RetValue == 1 && Abc_LatchIsInit0(pLatch)) ||
+ (RetValue == 0 && Abc_LatchIsInit1(pLatch)) )
+ {
+ // fanin constant differs from the latch init value
+ if ( pLatchPivot == NULL )
+ {
+ pLatchPivot = pLatch;
+ continue;
+ }
+ if ( Abc_LatchInit(pLatch) != Abc_LatchInit(pLatchPivot) ) // add inverter
+ pFanin = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanout0(pLatchPivot) );
+ else
+ pFanin = Abc_ObjFanout0(pLatchPivot);
+ }
+ else
+ pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
+ // replace latch
+ Abc_ObjTransferFanout( Abc_ObjFanout0(pLatch), pFanin );
+ // delete the extra nodes
+ Abc_NtkDeleteObj_rec( Abc_ObjFanout0(pLatch), 0 );
+ Counter++;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Replaces autonumnous logic by free inputs.]
+
+ Description [Assumes that non-autonomous logic is marked with
+ the current ID.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode, * pFanin;
+ Vec_Ptr_t * vNodes;
+ int i, k, Counter;
+ // collect the nodes that feed into the reachable logic
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NtkForEachObj( pNtk, pNode, i )
+ {
+ // skip non-visited fanins
+ if ( !Abc_NodeIsTravIdCurrent(pNode) )
+ continue;
+ // look for non-visited fanins
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ {
+ // skip visited fanins
+ if ( Abc_NodeIsTravIdCurrent(pFanin) )
+ continue;
+ // skip constants and latches fed by constants
+ if ( Abc_NtkCheckConstant_rec(pFanin) != -1 ||
+ (Abc_ObjIsBi(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) )
+ {
+ Abc_NtkSetTravId_rec( pFanin );
+ continue;
+ }
+ assert( !Abc_ObjIsLatch(pFanin) );
+ Vec_PtrPush( vNodes, pFanin );
+ }
+ }
+ Vec_PtrUniqify( vNodes, Abc_ObjPointerCompare );
+ // replace these nodes by the PIs
+ Vec_PtrForEachEntry( vNodes, pNode, i )
+ {
+ pFanin = Abc_NtkCreatePi(pNtk);
+ Abc_NodeSetTravIdCurrent( pFanin );
+ Abc_ObjTransferFanout( pNode, pFanin );
+ }
+ Counter = Vec_PtrSize(vNodes);
+ Vec_PtrFree( vNodes );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Sequential cleanup.]
+
+ Description [Performs three tasks:
+ - Removes logic that does not feed into POs.
+ - Removes latches driven by constant values equal to the initial state.
+ - Replaces the autonomous components by additional PI variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Vec_Ptr_t * vNodes;
+ int Counter;
+ assert( Abc_NtkIsLogic(pNtk) );
+ // mark the nodes reachable from the POs
+ vNodes = Abc_NtkDfsSeq( pNtk );
+ Vec_PtrFree( vNodes );
+ // remove the non-marked nodes
+ Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
+ if ( fVerbose )
+ printf( "Cleanup removed %4d dangling objects.\n", Counter );
+ // check if some of the latches can be removed
+ Counter = Abc_NtkLatchSweep( pNtk );
+ if ( fVerbose )
+ printf( "Cleanup removed %4d redundant latches.\n", Counter );
+ // detect the autonomous components
+ vNodes = Abc_NtkDfsSeqReverse( pNtk );
+ Vec_PtrFree( vNodes );
+ // replace them by PIs
+ Counter = Abc_NtkReplaceAutonomousLogic( pNtk );
+ if ( fVerbose )
+ printf( "Cleanup added %4d additional PIs.\n", Counter );
+ // remove the non-marked nodes
+ Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
+ if ( fVerbose )
+ printf( "Cleanup removed %4d autonomous objects.\n", Counter );
+ // check
+ if ( !Abc_NtkCheck( pNtk ) )
+ printf( "Abc_NtkCleanupSeq: The network check has failed.\n" );
+ return 1;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 622b4103..594cc2d6 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -333,7 +333,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
printf( "Networks are NOT EQUIVALENT after framing.\n" );
// report the error
pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
- Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
+// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
FREE( pFrames->pModel );
Abc_NtkDelete( pFrames );
return;
@@ -365,7 +365,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
- Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
+// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
}
else assert( 0 );
// delete the fraig manager
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
new file mode 100644
index 00000000..1d56ba36
--- /dev/null
+++ b/src/base/abci/abcXsim.c
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+ FileName [abcXsim.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Using X-valued simulation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcXsim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define XVS0 1
+#define XVS1 2
+#define XVSX 3
+
+static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value ) { pObj->pCopy = (void *)Value; }
+static inline int Abc_ObjGetXsim( Abc_Obj_t * pObj ) { return (int)pObj->pCopy; }
+static inline int Abc_XsimInv( int Value )
+{
+ if ( Value == XVS0 )
+ return XVS1;
+ if ( Value == XVS1 )
+ return XVS0;
+ assert( Value == XVSX );
+ return XVSX;
+}
+static inline int Abc_XsimAnd( int Value0, int Value1 )
+{
+ if ( Value0 == XVS0 || Value1 == XVS0 )
+ return XVS0;
+ if ( Value0 == XVSX || Value1 == XVSX )
+ return XVSX;
+ assert( Value0 == XVS1 && Value1 == XVS1 );
+ return XVS1;
+}
+static inline int Abc_XsimRand2()
+{
+ return (rand() & 1) ? XVS1 : XVS0;
+}
+static inline int Abc_XsimRand3()
+{
+ int RetValue;
+ do {
+ RetValue = rand() & 3;
+ } while ( RetValue == 0 );
+ return RetValue;
+}
+static inline int Abc_ObjGetXsimFanin0( Abc_Obj_t * pObj )
+{
+ int RetValue;
+ RetValue = Abc_ObjGetXsim(Abc_ObjFanin0(pObj));
+ return Abc_ObjFaninC0(pObj)? Abc_XsimInv(RetValue) : RetValue;
+}
+static inline int Abc_ObjGetXsimFanin1( Abc_Obj_t * pObj )
+{
+ int RetValue;
+ RetValue = Abc_ObjGetXsim(Abc_ObjFanin1(pObj));
+ return Abc_ObjFaninC1(pObj)? Abc_XsimInv(RetValue) : RetValue;
+}
+static inline void Abc_XsimPrint( FILE * pFile, int Value )
+{
+ if ( Value == XVS0 )
+ {
+ fprintf( pFile, "0" );
+ return;
+ }
+ if ( Value == XVS1 )
+ {
+ fprintf( pFile, "1" );
+ return;
+ }
+ assert( Value == XVSX );
+ fprintf( pFile, "x" );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs X-valued simulation of the sequential network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose )
+{
+ Abc_Obj_t * pObj;
+ int i, f;
+ assert( Abc_NtkIsStrash(pNtk) );
+ srand( 0x12341234 );
+ // start simulation
+ Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
+ if ( fInputs )
+ {
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, XVSX );
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
+ }
+ else
+ {
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX );
+ }
+ // simulate and print the result
+ fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Abc_AigForEachAnd( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) );
+ // print out
+ fprintf( stdout, "%2d : ", f );
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+ fprintf( stdout, " : " );
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) );
+ fprintf( stdout, " : " );
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+ fprintf( stdout, "\n" );
+ // assign input values
+ if ( fInputs )
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, XVSX );
+ else
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+ // transfer the latch values
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
+ }
+}
+
+///////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index bb2ae1a0..50a40393 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -2,6 +2,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcAttach.c \
src/base/abci/abcAuto.c \
src/base/abci/abcBalance.c \
+ src/base/abci/abcBmc.c \
src/base/abci/abcClpBdd.c \
src/base/abci/abcClpSop.c \
src/base/abci/abcCut.c \
@@ -37,4 +38,5 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcTiming.c \
src/base/abci/abcUnate.c \
src/base/abci/abcUnreach.c \
- src/base/abci/abcVerify.c
+ src/base/abci/abcVerify.c \
+ src/base/abci/abcXsim.c
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index cc51cc1c..f2f07b14 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -179,7 +179,7 @@ Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesI
Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 )
{
Abc_Obj_t * pNet, * pTerm;
- pTerm = fConst1? Abc_NodeCreateConst1(pNtk) : Abc_NodeCreateConst0(pNtk);
+ pTerm = fConst1? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
pNet = Abc_NtkFindNet(pNtk, pName); assert( pNet );
Abc_ObjAddFanin( pNet, pTerm );
return pTerm;
@@ -200,7 +200,7 @@ Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut
{
Abc_Obj_t * pNet, * pNode;
pNet = Abc_NtkFindNet(pNtk, pNameIn); assert( pNet );
- pNode = Abc_NodeCreateInv(pNtk, pNet);
+ pNode = Abc_NtkCreateNodeInv(pNtk, pNet);
pNet = Abc_NtkFindNet(pNtk, pNameOut); assert( pNet );
Abc_ObjAddFanin( pNet, pNode );
return pNode;
@@ -221,7 +221,7 @@ Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut
{
Abc_Obj_t * pNet, * pNode;
pNet = Abc_NtkFindNet(pNtk, pNameIn); assert( pNet );
- pNode = Abc_NodeCreateBuf(pNtk, pNet);
+ pNode = Abc_NtkCreateNodeBuf(pNtk, pNet);
pNet = Abc_NtkFindNet(pNtk, pNameOut); assert( pNet );
Abc_ObjAddFanin( pNet, pNode );
return pNet;
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 8ce837e2..05539c40 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -112,10 +112,13 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fprintf( pFile, "\n" );
fprintf( pFile, "digraph AIG {\n" );
fprintf( pFile, "size = \"7.5,10\";\n" );
+// fprintf( pFile, "size = \"10,8.5\";\n" );
+// fprintf( pFile, "size = \"14,11\";\n" );
+// fprintf( pFile, "page = \"8,11\";\n" );
// fprintf( pFile, "ranksep = 0.5;\n" );
// fprintf( pFile, "nodesep = 0.5;\n" );
fprintf( pFile, "center = true;\n" );
-// fprintf( pFile, "orientation = landscape;\n" );
+// fprintf( pFile, "orientation = landscape;\n" );
// fprintf( pFile, "edge [fontsize = 10];\n" );
// fprintf( pFile, "edge [dir = none];\n" );
fprintf( pFile, "edge [dir = back];\n" );
@@ -320,8 +323,8 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fprintf( pFile, "Node%d%s", Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
- if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL0(pNode) > 0 )
- fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
+// if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL0(pNode) > 0 )
+// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
}
@@ -335,8 +338,8 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fprintf( pFile, "Node%d%s", Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
fprintf( pFile, " [" );
fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
- if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL1(pNode) > 0 )
- fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
+// if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL1(pNode) > 0 )
+// fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
fprintf( pFile, "]" );
fprintf( pFile, ";\n" );
}
diff --git a/src/base/seq/seqUtil.c b/src/base/seq/seqUtil.c
index af2a0a7a..55b9df8e 100644
--- a/src/base/seq/seqUtil.c
+++ b/src/base/seq/seqUtil.c
@@ -580,7 +580,8 @@ int Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
Abc_NtkNodeNum(pNtk), Vec_PtrSize(vNodesPo), Vec_PtrSize(vNodesPi) );
if ( Abc_NtkNodeNum(pNtk) > Vec_PtrSize(vNodesPo) )
{
- Counter = Abc_NtkReduceNodes( pNtk, vNodesPo );
+// Counter = Abc_NtkReduceNodes( pNtk, vNodesPo );
+ Counter = 0;
if ( fVerbose )
printf( "Cleanup removed %d nodes that are not reachable from the POs.\n", Counter );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-02 08:02:30 +0000