summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abc.h99
-rw-r--r--src/base/abc/abcAig.c8
-rw-r--r--src/base/abc/abcCheck.c4
-rw-r--r--src/base/abc/abcFanio.c41
-rw-r--r--src/base/abc/abcLib.c207
-rw-r--r--src/base/abc/abcNames.c11
-rw-r--r--src/base/abc/abcNetlist.c6
-rw-r--r--src/base/abc/abcNtk.c87
-rw-r--r--src/base/abc/abcObj.c474
-rw-r--r--src/base/abci/abcMiter.c14
-rw-r--r--src/base/abci/abcNtbdd.c2
-rw-r--r--src/base/abci/abcPrint.c5
-rw-r--r--src/base/abci/abcRr.c2
-rw-r--r--src/base/abci/abcSat.c13
-rw-r--r--src/base/abci/abcStrash.c4
-rw-r--r--src/base/abci/abcUnreach.c2
-rw-r--r--src/base/abci/abcVanEijk.c4
-rw-r--r--src/base/abci/abcVanImp.c2
-rw-r--r--src/base/io/io.c38
-rw-r--r--src/base/io/io.h2
-rw-r--r--src/base/io/ioReadBaf.c2
-rw-r--r--src/base/io/ioReadBlif.c2
-rw-r--r--src/base/io/ioReadVerilog.c2
-rw-r--r--src/base/io/ioWriteVer.c89
-rw-r--r--src/base/seq/seqAigCore.c2
-rw-r--r--src/base/seq/seqCreate.c4
-rw-r--r--src/base/seq/seqRetCore.c2
-rw-r--r--src/misc/extra/extraUtilMemory.c2
-rw-r--r--src/misc/vec/vecInt.h12
-rw-r--r--src/sat/csat/csat_apis.c2
-rw-r--r--src/temp/aig/aig.h4
-rw-r--r--src/temp/aig/aigUtil.c173
-rw-r--r--src/temp/ver/ver.h7
-rw-r--r--src/temp/ver/verCore.c157
-rw-r--r--src/temp/ver/verFormula.c53
35 files changed, 1032 insertions, 506 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 10e2eb41..e106d5eb 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -90,12 +90,12 @@ typedef enum {
ABC_OBJ_PO, // 4: primary output terminal
ABC_OBJ_BI, // 5: box input terminal
ABC_OBJ_BO, // 6: box output terminal
- ABC_OBJ_NET, // 7: net
- ABC_OBJ_NODE, // 8: node
- ABC_OBJ_LATCH, // 9: latch
- ABC_OBJ_ASSERT, // 10: assertion output
+ ABC_OBJ_ASSERT, // 7: assertion output
+ ABC_OBJ_NET, // 8: net
+ ABC_OBJ_NODE, // 9: node
+ ABC_OBJ_LATCH, // 10: latch
ABC_OBJ_BOX, // 11: box
- ABC_OBJ_OTHER // 12: unused
+ ABC_OBJ_NUMBER // 12: unused
} Abc_ObjType_t;
// latch initial values
@@ -166,7 +166,6 @@ struct Abc_Ntk_t_
Abc_NtkFunc_t ntkFunc; // functionality of the network
char * pName; // the network name
char * pSpec; // the name of the spec file if present
- int Id; // network ID
Nm_Man_t * pManName; // name manager (stores names of objects)
// components of the network
Vec_Ptr_t * vObjs; // the array of all objects (net, nodes, latches, etc)
@@ -181,9 +180,7 @@ struct Abc_Ntk_t_
Vec_Ptr_t * vCutSet; // the array of cutset nodes (used in the sequential AIG)
// the number of living objects
int nObjs; // the number of live objs
- int nNets; // the number of live nets
- int nNodes; // the number of live nodes
- int nBoxes; // the number of live nodes
+ int nObjCounts[ABC_OBJ_NUMBER]; // the number of objects by type
// the backup network and the step number
Abc_Ntk_t * pNetBackup; // the pointer to the previous backup network
int iStep; // the generation number for the given network
@@ -197,6 +194,7 @@ struct Abc_Ntk_t_
Extra_MmFixed_t * pMmObj; // memory manager for objects
Extra_MmStep_t * pMmStep; // memory manager for arrays
void * pManFunc; // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
+// Abc_Lib_t * pVerLib; // for structural verilog designs
void * pManGlob; // the global BDD manager
Vec_Ptr_t * vFuncsGlob; // the global BDDs of CO functions
Abc_ManTime_t * pManTime; // the timing manager (for mapped networks) stores arrival/required times for all nodes
@@ -206,6 +204,7 @@ struct Abc_Ntk_t_
Vec_Ptr_t * vSupps; // CO support information
int * pModel; // counter-example (for miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
+ void * pData; // misc
// skew values (for latches)
float maxMeanCycle; // maximum mean cycle time
float globalSkew; // global skewing
@@ -215,8 +214,10 @@ struct Abc_Ntk_t_
struct Abc_Lib_t_
{
char * pName; // the name of the library
- void * pManFunc; // functionality manager for the gates
- st_table * tModules; // the table hashing gate/module names into their networks
+ void * pManFunc; // functionality manager for the nodes
+ Vec_Ptr_t * vModules; // the array of modules
+ st_table * tModules; // the table hashing module names into their networks
+ Abc_Lib_t * pLibrary; // the library used to map this design
};
////////////////////////////////////////////////////////////////////////
@@ -229,21 +230,25 @@ struct Abc_Lib_t_
#define ABC_INFINITY (100000000)
// transforming floats into ints and back
-static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); }
-static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); }
-static inline int Abc_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
+static inline int Abc_Float2Int( float Val ) { return *((int *)&Val); }
+static inline float Abc_Int2Float( int Num ) { return *((float *)&Num); }
+static inline int Abc_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); }
+static inline int Abc_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
+static inline int Abc_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
+static inline void Abc_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
+static inline void Abc_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
// checking the network type
-static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; }
-static inline bool Abc_NtkIsLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_LOGIC; }
-static inline bool Abc_NtkIsStrash( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_STRASH; }
-static inline bool Abc_NtkIsSeq( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_SEQ; }
+static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; }
+static inline bool Abc_NtkIsLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_LOGIC; }
+static inline bool Abc_NtkIsStrash( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_STRASH; }
+static inline bool Abc_NtkIsSeq( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_SEQ; }
-static inline bool Abc_NtkHasSop( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_SOP; }
-static inline bool Abc_NtkHasBdd( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_BDD; }
-static inline bool Abc_NtkHasAig( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_AIG; }
-static inline bool Abc_NtkHasMapping( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_MAP; }
-static inline bool Abc_NtkHasBlackbox( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_BLACKBOX; }
+static inline bool Abc_NtkHasSop( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_SOP; }
+static inline bool Abc_NtkHasBdd( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_BDD; }
+static inline bool Abc_NtkHasAig( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_AIG; }
+static inline bool Abc_NtkHasMapping( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_MAP; }
+static inline bool Abc_NtkHasBlackbox( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_BLACKBOX; }
static inline bool Abc_NtkIsSopNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_NTK_NETLIST; }
static inline bool Abc_NtkIsAigNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_AIG && pNtk->ntkType == ABC_NTK_NETLIST; }
@@ -252,7 +257,7 @@ static inline bool Abc_NtkIsSopLogic( Abc_Ntk_t * pNtk ) { return pN
static inline bool Abc_NtkIsBddLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_BDD && pNtk->ntkType == ABC_NTK_LOGIC ; }
static inline bool Abc_NtkIsAigLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_AIG && pNtk->ntkType == ABC_NTK_LOGIC ; }
static inline bool Abc_NtkIsMappedLogic( Abc_Ntk_t * pNtk ) { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_NTK_LOGIC ; }
-static inline bool Abc_NtkIsComb( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vLatches) == 0; }
+static inline bool Abc_NtkIsComb( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vLatches) == 0; }
// reading data members of the network
static inline char * Abc_NtkName( Abc_Ntk_t * pNtk ) { return pNtk->pName; }
@@ -271,19 +276,20 @@ static inline void Abc_NtkSetStep ( Abc_Ntk_t * pNtk, int iStep )
// getting the number of objects
static inline int Abc_NtkObjNumMax( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vObjs); }
static inline int Abc_NtkObjNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjs; }
-static inline int Abc_NtkNetNum( Abc_Ntk_t * pNtk ) { return pNtk->nNets; }
-static inline int Abc_NtkNodeNum( Abc_Ntk_t * pNtk ) { return pNtk->nNodes; }
-static inline int Abc_NtkLatchNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vLatches); }
-static inline int Abc_NtkAssertNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vAsserts); }
-static inline int Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCutSet); }
+static inline int Abc_NtkNetNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_NET]; }
+static inline int Abc_NtkNodeNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_NODE]; }
+static inline int Abc_NtkBoxNum( Abc_Ntk_t * pNtk ) { return pNtk->nObjCounts[ABC_OBJ_BOX]; }
static inline int Abc_NtkPiNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vPis); }
static inline int Abc_NtkPoNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vPos); }
static inline int Abc_NtkCiNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCis); }
static inline int Abc_NtkCoNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCos); }
-static inline int Abc_NtkBoxNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vBoxes); }
+static inline int Abc_NtkLatchNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vLatches); }
+static inline int Abc_NtkAssertNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vAsserts); }
+static inline int Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk ) { return Vec_PtrSize(pNtk->vCutSet); }
// reading objects
static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vObjs, i ); }
+static inline Abc_Obj_t * Abc_NtkBox( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i ); }
static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vLatches, i );}
static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i ) { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vAsserts, i );}
static inline Abc_Obj_t * Abc_NtkCutSetNode( Abc_Ntk_t * pNtk, int i){ return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCutSet, i ); }
@@ -353,6 +359,18 @@ static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Ab
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) ); }
+// creating simple objects
+extern inline Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+static inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) { return Abc_NtkObjAdd( pNtk, Type ); }
+static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_NODE ); }
+static inline Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BOX ); }
+static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_PI ); }
+static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_PO ); }
+static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BI ); }
+static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_BO ); }
+static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_LATCH ); }
+static Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk ) { return Abc_NtkObjAdd( pNtk, ABC_OBJ_ASSERT ); }
+
// checking the AIG node types
static inline bool Abc_AigNodeIsConst( Abc_Obj_t * pNode ) { assert(Abc_NtkIsStrash(Abc_ObjRegular(pNode)->pNtk)||Abc_NtkIsSeq(Abc_ObjRegular(pNode)->pNtk)); return Abc_ObjRegular(pNode)->Type == ABC_OBJ_CONST1; }
static inline bool Abc_AigNodeIsAnd( Abc_Obj_t * pNode ) { assert(!Abc_ObjIsComplement(pNode)); assert(Abc_NtkIsStrash(pNode->pNtk)||Abc_NtkIsSeq(pNode->pNtk)); return Abc_ObjFaninNum(pNode) == 2; }
@@ -405,9 +423,9 @@ static inline float Abc_NtkGetLatSkew ( Abc_Ntk_t * pNtk, int lat )
#define Abc_AigForEachAnd( pNtk, pNode, i ) \
for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ ) \
if ( (pNode) == NULL || !Abc_AigNodeIsAnd(pNode) ) {} else
-#define Abc_NtkForEachBox( pNtk, pNode, i ) \
- for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ ) \
- if ( (pNode) == NULL || !Abc_ObjIsBox(pNode) ) {} else
+#define Abc_NtkForEachBox( pNtk, pNode, i ) \
+ for ( i = 0; (i < Vec_PtrSize((pNtk)->vBoxes)) && (((pNode) = Abc_NtkBox(pNtk, i)), 1); i++ ) \
+ if ( (pNode) == NULL ) {} else
#define Abc_SeqForEachCutsetNode( pNtk, pNode, i ) \
for ( i = 0; (i < Abc_NtkCutSetNodeNum(pNtk)) && (((pNode) = Abc_NtkCutSetNode(pNtk, i)), 1); i++ )\
if ( (pNode) == NULL ) {} else
@@ -498,6 +516,7 @@ extern void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin
extern void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
extern void Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
extern void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
+extern Abc_Obj_t * Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type );
extern void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
extern void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
/*=== abcFraig.c ==========================================================*/
@@ -549,21 +568,15 @@ extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fIni
/*=== abcObj.c ==========================================================*/
extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
extern void Abc_ObjRecycle( Abc_Obj_t * pObj );
-extern void Abc_ObjAdd( Abc_Obj_t * pObj );
-extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
-extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
+extern Abc_Obj_t * Abc_NtkObjAdd( 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 Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
+extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindTerm( Abc_Ntk_t * pNtk, char * pName );
extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk );
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 );
@@ -611,7 +624,7 @@ extern Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
extern DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly, int fReorder, int fVerbose );
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_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan );
extern Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
extern Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
extern Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 75e0292e..7a261cf4 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -136,12 +136,10 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
pMan->vStackReplaceOld = Vec_PtrAlloc( 100 );
pMan->vStackReplaceNew = Vec_PtrAlloc( 100 );
// create the constant node
- pMan->pConst1 = Abc_ObjAlloc( pNtkAig, ABC_OBJ_CONST1 );
- // add to the array of objects, count it as object but not as node
assert( pNtkAig->vObjs->nSize == 0 );
- pMan->pConst1->Id = pNtkAig->vObjs->nSize;
- Vec_PtrPush( pNtkAig->vObjs, pMan->pConst1 );
- pNtkAig->nObjs++;
+ pMan->pConst1 = Abc_NtkObjAdd( pNtkAig, ABC_OBJ_NODE );
+ pMan->pConst1->Type = ABC_OBJ_CONST1;
+ pNtkAig->nObjCounts[ABC_OBJ_NODE]--;
// save the current network
pMan->pNtkAig = pNtkAig;
return pMan;
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index af6f4ef7..12a2fab7 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -117,14 +117,14 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
{
fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
fprintf( stdout, "One possible reason is that latches are added twice:\n" );
- fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+ fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" );
return 0;
}
if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
{
fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
fprintf( stdout, "One possible reason is that latches are added twice:\n" );
- fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+ fprintf( stdout, "in procedure Abc_NtkObjAdd() and in the user's code.\n" );
return 0;
}
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 1d2ae23b..8e78ae61 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -167,6 +167,47 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
/**Function*************************************************************
+ Synopsis [Inserts one-input node of the type specified between the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type )
+{
+ Abc_Obj_t * pNodeNew;
+ int iFanoutIndex, iFaninIndex;
+ // find pNodeOut among the fanouts of pNodeIn
+ if ( (iFanoutIndex = Vec_IntFind( &pNodeIn->vFanouts, pNodeOut->Id )) == -1 )
+ {
+ printf( "Node %s is not among", Abc_ObjName(pNodeOut) );
+ printf( " the fanouts of node %s...\n", Abc_ObjName(pNodeIn) );
+ return NULL;
+ }
+ // find pNodeIn among the fanins of pNodeOut
+ if ( (iFaninIndex = Vec_IntFind( &pNodeOut->vFanins, pNodeIn->Id )) == -1 )
+ {
+ printf( "Node %s is not among", Abc_ObjName(pNodeIn) );
+ printf( " the fanins of node %s...\n", Abc_ObjName(pNodeOut) );
+ return NULL;
+ }
+ // create the new node
+ pNodeNew = Abc_NtkCreateObj( pNodeIn->pNtk, Type );
+ // add pNodeIn as fanin and pNodeOut as fanout
+ Vec_IntPushMem( pNodeNew->pNtk->pMmStep, &pNodeNew->vFanins, pNodeIn->Id );
+ Vec_IntPushMem( pNodeNew->pNtk->pMmStep, &pNodeNew->vFanouts, pNodeOut->Id );
+ // update the fanout of pNodeIn
+ Vec_IntWriteEntry( &pNodeIn->vFanouts, iFanoutIndex, pNodeNew->Id );
+ // update the fanin of pNodeOut
+ Vec_IntWriteEntry( &pNodeOut->vFanins, iFaninIndex, pNodeNew->Id );
+ return pNodeNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Transfers fanout from the old node to the new node.]
Description []
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index 80bcc516..1d6619f0 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -46,7 +46,9 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
memset( p, 0, sizeof(Abc_Lib_t) );
p->pName = Extra_UtilStrsav( pName );
p->tModules = st_init_table( strcmp, st_strhash );
+ p->vModules = Vec_PtrAlloc( 100 );
p->pManFunc = Aig_ManStart();
+ p->pLibrary = NULL;
return p;
}
@@ -63,18 +65,22 @@ Abc_Lib_t * Abc_LibCreate( char * pName )
***********************************************************************/
void Abc_LibFree( Abc_Lib_t * pLib )
{
- st_generator * gen;
Abc_Ntk_t * pNtk;
- char * pName;
+ int i;
if ( pLib->pName )
free( pLib->pName );
if ( pLib->pManFunc )
Aig_ManStop( pLib->pManFunc );
if ( pLib->tModules )
+ st_free_table( pLib->tModules );
+ if ( pLib->vModules )
{
- st_foreach_item( pLib->tModules, gen, (char**)&pName, (char**)&pNtk )
+ Vec_PtrForEachEntry( pLib->vModules, pNtk, i )
+ {
+ pNtk->pManFunc = NULL;
Abc_NtkDelete( pNtk );
- st_free_table( pLib->tModules );
+ }
+ Vec_PtrFree( pLib->vModules );
}
free( pLib );
}
@@ -92,21 +98,198 @@ void Abc_LibFree( Abc_Lib_t * pLib )
***********************************************************************/
Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib )
{
- st_generator * gen;
Abc_Ntk_t * pNtk;
- char * pName;
- if ( st_count(pLib->tModules) > 1 )
+ if ( Vec_PtrSize(pLib->vModules) > 1 )
{
printf( "The design includes more than one module and is currently not used.\n" );
return NULL;
}
- // find the network
- st_foreach_item( pLib->tModules, gen, (char**)&pName, (char**)&pNtk )
+ pNtk = Vec_PtrEntry( pLib->vModules, 0 ); Vec_PtrClear( pLib->vModules );
+ pNtk->pManFunc = pLib->pManFunc; pLib->pManFunc = NULL;
+ return pNtk;
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Surround boxes without content (black boxes) with BIs/BOs.]
+
+ Description [Returns the number of black boxes converted.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
+{
+ Abc_Obj_t * pObj, * pFanin, * pFanout;
+ int i, k;
+ assert( Abc_NtkIsNetlist(pNtk) );
+ // collect blackbox nodes
+ assert( Vec_PtrSize(pNtk->vBoxes) == 0 );
+ Vec_PtrClear( pNtk->vBoxes );
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ if ( Abc_NtkNodeNum(pObj->pData) == 0 )
+ Vec_PtrPush( pNtk->vBoxes, pObj );
+ // return if there is no black boxes without content
+ if ( Vec_PtrSize(pNtk->vBoxes) == 0 )
+ return 0;
+ // print the boxes
+ printf( "Black boxes are: " );
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ printf( " %s", ((Abc_Ntk_t *)pObj->pData)->pName );
+ printf( "\n" );
+ // iterate through the boxes and add BIs/BOs
+ Abc_NtkForEachBox( pNtk, pObj, i )
{
- st_free_gen(gen);
- break;
+ // go through the fanin nets
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BO );
+ // go through the fanout nets
+ Abc_ObjForEachFanout( pObj, pFanout, k )
+ {
+ Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BI );
+ // if the name is not given assign name
+ if ( pFanout->pData == NULL )
+ {
+ pFanout->pData = Abc_ObjName( pFanout );
+ Nm_ManStoreIdName( pNtk->pManName, pFanout->Id, pFanout->pData, NULL );
+ }
+ }
}
- return pNtk;
+ return Vec_PtrSize(pNtk->vBoxes);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derive the AIG of the logic in the netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeStrashUsingNetwork_rec( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObj )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ assert( !Abc_ObjIsNet(pObj) );
+ if ( pObj->pCopy )
+ return;
+ // call for the fanins
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
+ // compute for the node
+ pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+ // set for the fanout net
+ Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derive the AIG of the logic in the netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeStrashUsingNetwork( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pBox )
+{
+ Abc_Ntk_t * pNtkGate;
+ Abc_Obj_t * pObj;
+ unsigned * pPolarity;
+ int i, fCompl;
+ assert( Abc_ObjIsBox(pBox) );
+ pNtkGate = pBox->pData;
+ pPolarity = (unsigned *)pBox->pNext;
+ assert( Abc_NtkIsNetlist(pNtkGate) );
+ assert( Abc_NtkLatchNum(pNtkGate) == 0 );
+ Abc_NtkCleanCopy( pNtkGate );
+ // set the PI values
+ Abc_NtkForEachPi( pNtkGate, pObj, i )
+ {
+ fCompl = (pPolarity && Abc_InfoHasBit(pPolarity, i));
+ pObj->pCopy = Abc_ObjNotCond( Abc_ObjFanin(pBox,i)->pCopy, fCompl );
+ Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+ }
+ // build recursively and set the PO values
+ Abc_NtkForEachPo( pNtkGate, pObj, i )
+ {
+ Abc_NodeStrashUsingNetwork_rec( pNtkAig, Abc_ObjFanin0Ntk(Abc_ObjFanin0(pObj)) );
+ Abc_ObjFanout(pBox,i)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derive the AIG of the logic in the netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
+{
+ ProgressBar * pProgress;
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkAig;
+ Abc_Obj_t * pObj;
+ int i, nBoxes;
+ // explicitly derive black boxes
+ assert( Abc_NtkIsNetlist(pNtk) );
+ nBoxes = Abc_LibDeriveBlackBoxes( pNtk, pLib );
+ if ( nBoxes )
+ printf( "Detected and transformed %d black boxes.\n", nBoxes );
+ // create the new network with black boxes in place
+ pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ // transer to the nets
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+ // build the AIG for the remaining logic in the netlist
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ if ( Abc_ObjIsNode(pObj) )
+ {
+ pObj->pCopy = Abc_NodeStrash( pNtkAig, pObj );
+ Abc_ObjFanout0(pObj)->pCopy = pObj->pCopy;
+ continue;
+ }
+ Abc_NodeStrashUsingNetwork( pNtkAig, pObj );
+ }
+ Extra_ProgressBarStop( pProgress );
+ Vec_PtrFree( vNodes );
+ // deallocate memory manager, which remembers the phase
+ if ( pNtk->pData )
+ {
+ Extra_MmFlexStop( pNtk->pData, 0 );
+ pNtk->pData = NULL;
+ }
+ // set the COs
+// Abc_NtkFinalize( pNtk, pNtkAig );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+ Abc_AigCleanup( pNtkAig->pManFunc );
+ // make sure that everything is okay
+ if ( !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_LibDeriveAig: The network check has failed.\n" );
+ return 0;
+ }
+ return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index ef1d0980..0deb20e3 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -166,8 +166,8 @@ char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * p
***********************************************************************/
void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
{
- Abc_Obj_t * pObj;
- int i;
+ Abc_Obj_t * pObj, * pTerm;
+ int i, k;
assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) );
@@ -181,6 +181,13 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
Abc_NtkForEachAssert( pNtk, pObj, i )
Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i), Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ {
+ Abc_ObjForEachFanin( pObj, pTerm, k )
+ Abc_NtkLogicStoreName( pTerm->pCopy, Abc_ObjName(Abc_ObjFanin0Ntk(pTerm)) );
+ Abc_ObjForEachFanout( pObj, pTerm, k )
+ Abc_NtkLogicStoreName( pTerm->pCopy, Abc_ObjName(Abc_ObjFanout0Ntk(pTerm)) );
+ }
if ( !Abc_NtkIsSeq(pNtk) )
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 456d2aa2..145531db 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -95,11 +95,11 @@ Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
int i, Counter = 0;
assert( Abc_NtkIsNetlist(pNtk) );
// start the network
-// pNtkNew = Abc_NtkAlloc( Type, Func );
+// pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
if ( !Abc_NtkHasMapping(pNtk) )
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
else
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index f21d79be..e94e0a2f 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -43,7 +43,7 @@
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan )
{
Abc_Ntk_t * pNtk;
pNtk = ALLOC( Abc_Ntk_t, 1 );
@@ -63,8 +63,8 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
pNtk->vBoxes = Vec_PtrAlloc( 100 );
pNtk->vSkews = Vec_FltAlloc( 100 );
// start the memory managers
- pNtk->pMmObj = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
- pNtk->pMmStep = Extra_MmStepStart( ABC_NUM_STEPS );
+ pNtk->pMmObj = fUseMemMan? Extra_MmFixedStart( sizeof(Abc_Obj_t) ) : NULL;
+ pNtk->pMmStep = fUseMemMan? Extra_MmStepStart( ABC_NUM_STEPS ) : NULL;
// get ready to assign the first Obj ID
pNtk->nTravIds = 1;
// start the functionality manager
@@ -101,12 +101,12 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
{
Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObj;
- int i;
+ Abc_Obj_t * pObj, * pTerm;
+ int i, k;
if ( pNtk == NULL )
return NULL;
// start the network
- pNtkNew = Abc_NtkAlloc( Type, Func );
+ pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -125,6 +125,16 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
Abc_NtkDupObj(pNtkNew, pObj);
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_NtkDupObj(pNtkNew, pObj);
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ {
+ Abc_NtkDupObj(pNtkNew, pObj);
+ if ( Abc_NtkIsNetlist(pNtk) )
+ continue;
+ Abc_ObjForEachFanin( pObj, pTerm, k )
+ Abc_NtkDupObj(pNtkNew, pTerm);
+ Abc_ObjForEachFanout( pObj, pTerm, k )
+ Abc_NtkDupObj(pNtkNew, pTerm);
+ }
// transfer the names
if ( Type != ABC_NTK_NETLIST )
Abc_NtkDupCioNamesTable( pNtk, pNtkNew );
@@ -155,7 +165,7 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
if ( pNtk == NULL )
return NULL;
// start the network
- pNtkNew = Abc_NtkAlloc( Type, Func );
+ pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -172,6 +182,8 @@ Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc
Abc_NtkDupObj(pNtkNew, pObj);
Abc_NtkForEachAssert( pNtk, pObj, i )
Abc_NtkDupObj(pNtkNew, pObj);
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ Abc_NtkDupObj(pNtkNew, pObj);
// transfer the names
if ( Type != ABC_NTK_NETLIST )
Abc_NtkDupCioNamesTableNoLatches( pNtk, pNtkNew );
@@ -201,7 +213,7 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
if ( pNtk == NULL )
return NULL;
// start the network
- pNtkNew = Abc_NtkAlloc( Type, Func );
+ pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = NULL;
@@ -228,6 +240,8 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
Abc_NtkDupObj(pNtkNew, pObj);
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_NtkDupObj(pNtkNew, pObj);
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ Abc_NtkDupObj(pNtkNew, pObj);
// transfer the names
Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
// check that the CI/CO/latches are copied correctly
@@ -276,7 +290,7 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
{
Abc_Ntk_t * pNtkNew;
// allocate the empty network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
// set the specs
pNtkNew->pName = Extra_FileNameGeneric(pName);
pNtkNew->pSpec = Extra_UtilStrsav(pName);
@@ -426,7 +440,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
assert( Abc_ObjIsNode(pNode) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
// set the name
sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName );
pNtkNew->pName = Extra_UtilStrsav(Buffer);
@@ -496,7 +510,7 @@ Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
assert( Abc_ObjIsNode(pNode) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
// set the name
sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName );
pNtkNew->pName = Extra_UtilStrsav(Buffer);
@@ -571,7 +585,7 @@ Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t
// start the network
Abc_NtkCleanCopy( pNtk );
- pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
// collect the nodes in the TFI of the output
@@ -626,7 +640,7 @@ Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
Abc_Obj_t * pFanin, * pNodePo;
int i;
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
pNtkNew->pName = Extra_UtilStrsav(Abc_ObjName(pNode));
// add the PIs corresponding to the fanins of the node
Abc_ObjForEachFanin( pNode, pFanin, i )
@@ -665,7 +679,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop )
Vec_Ptr_t * vNames;
int i, nVars;
// start the network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
pNtkNew->pName = Extra_UtilStrsav("ex");
// create PIs
Vec_PtrPush( pNtkNew->vObjs, NULL );
@@ -706,11 +720,20 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
int LargePiece = (4 << ABC_NUM_STEPS);
if ( pNtk == NULL )
return;
+ // free EXDC Ntk
+ if ( pNtk->pExdc )
+ Abc_NtkDelete( pNtk->pExdc );
+ // dereference the BDDs
+ if ( Abc_NtkHasBdd(pNtk) )
+ {
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+ }
// make sure all the marks are clean
Abc_NtkForEachObj( pNtk, pObj, i )
{
// free large fanout arrays
- if ( pObj->vFanouts.nCap * 4 > LargePiece )
+ if ( pNtk->pMmObj && pObj->vFanouts.nCap * 4 > LargePiece )
FREE( pObj->vFanouts.pArray );
// these flags should be always zero
// if this is not true, something is wrong somewhere
@@ -718,17 +741,23 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
assert( pObj->fMarkB == 0 );
assert( pObj->fMarkC == 0 );
}
-
- // dereference the BDDs
- if ( Abc_NtkHasBdd(pNtk) )
- Abc_NtkForEachNode( pNtk, pObj, i )
- Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+ // free the nodes
+ if ( pNtk->pMmStep == NULL )
+ {
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ FREE( pObj->vFanouts.pArray );
+ FREE( pObj->vFanins.pArray );
+ }
+ }
+ if ( pNtk->pMmObj == NULL )
+ {
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ free( pObj );
+ }
FREE( pNtk->pName );
FREE( pNtk->pSpec );
- // copy the EXDC Ntk
- if ( pNtk->pExdc )
- Abc_NtkDelete( pNtk->pExdc );
// free the arrays
Vec_PtrFree( pNtk->vPios );
Vec_PtrFree( pNtk->vPis );
@@ -743,12 +772,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
Vec_FltFree( pNtk->vSkews );
if ( pNtk->pModel ) free( pNtk->pModel );
TotalMemory = 0;
- TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
- TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
+ TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj) : 0;
+ TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
// fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
// free the storage
- Extra_MmFixedStop( pNtk->pMmObj, 0 );
- Extra_MmStepStop ( pNtk->pMmStep, 0 );
+ if ( pNtk->pMmObj )
+ Extra_MmFixedStop( pNtk->pMmObj, 0 );
+ if ( pNtk->pMmStep )
+ Extra_MmStepStop ( pNtk->pMmStep, 0 );
// name manager
Nm_ManFree( pNtk->pManName );
// free the timing manager
@@ -764,7 +795,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
else if ( Abc_NtkHasBdd(pNtk) )
Extra_StopManager( pNtk->pManFunc );
else if ( Abc_NtkHasAig(pNtk) )
- Aig_ManStop( pNtk->pManFunc );
+ { if ( pNtk->pManFunc ) Aig_ManStop( pNtk->pManFunc ); }
else if ( Abc_NtkHasMapping(pNtk) )
pNtk->pManFunc = NULL;
else if ( !Abc_NtkHasBlackbox(pNtk) )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 2811be16..27f5040c 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -33,7 +33,7 @@
/**Function*************************************************************
- Synopsis [Creates a new Obj.]
+ Synopsis [Creates a new object.]
Description []
@@ -45,7 +45,10 @@
Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
{
Abc_Obj_t * pObj;
- pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj );
+ if ( pNtk->pMmObj )
+ pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj );
+ else
+ pObj = (Abc_Obj_t *)ALLOC( Abc_Obj_t, 1 );
memset( pObj, 0, sizeof(Abc_Obj_t) );
pObj->pNtk = pNtk;
pObj->Type = Type;
@@ -55,7 +58,7 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
/**Function*************************************************************
- Synopsis [Recycles the Obj.]
+ Synopsis [Recycles the object.]
Description []
@@ -69,12 +72,20 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
Abc_Ntk_t * pNtk = pObj->pNtk;
int LargePiece = (4 << ABC_NUM_STEPS);
// free large fanout arrays
- if ( pObj->vFanouts.nCap * 4 > LargePiece )
+ if ( pNtk->pMmStep && pObj->vFanouts.nCap * 4 > LargePiece )
+ FREE( pObj->vFanouts.pArray );
+ if ( pNtk->pMmStep == NULL )
+ {
FREE( pObj->vFanouts.pArray );
+ FREE( pObj->vFanins.pArray );
+ }
// clean the memory to make deleted object distinct from the live one
memset( pObj, 0, sizeof(Abc_Obj_t) );
// recycle the object
- Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
+ if ( pNtk->pMmObj )
+ Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
+ else
+ free( pObj );
}
/**Function*************************************************************
@@ -88,58 +99,177 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Abc_ObjAdd( Abc_Obj_t * pObj )
+Abc_Obj_t * Abc_NtkObjAdd( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
{
- Abc_Ntk_t * pNtk = pObj->pNtk;
- assert( !Abc_ObjIsComplement(pObj) );
- // add to the array of objects
+ Abc_Obj_t * pObj;
+ // create new object, assign ID, and add to the array
+ pObj = Abc_ObjAlloc( pNtk, Type );
pObj->Id = pNtk->vObjs->nSize;
Vec_PtrPush( pNtk->vObjs, pObj );
+ pNtk->nObjCounts[Type]++;
pNtk->nObjs++;
// perform specialized operations depending on the object type
- if ( Abc_ObjIsNode(pObj) )
+ switch (Type)
{
- pNtk->nNodes++;
+ case ABC_OBJ_NONE:
+ assert(0);
+ break;
+ case ABC_OBJ_CONST1:
+ assert(0);
+ break;
+ case ABC_OBJ_PIO:
+ assert(0);
+ break;
+ case ABC_OBJ_PI:
+ Vec_PtrPush( pNtk->vPis, pObj );
+ Vec_PtrPush( pNtk->vCis, pObj );
+ break;
+ case ABC_OBJ_PO:
+ Vec_PtrPush( pNtk->vPos, pObj );
+ Vec_PtrPush( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_BI:
+ Vec_PtrPush( pNtk->vCis, pObj );
+ break;
+ case ABC_OBJ_BO:
+ Vec_PtrPush( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_ASSERT:
+ Vec_PtrPush( pNtk->vAsserts, pObj );
+ Vec_PtrPush( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_NET:
+ break;
+ case ABC_OBJ_NODE:
+ break;
+ case ABC_OBJ_LATCH:
+ pObj->pData = (void *)ABC_INIT_NONE;
+ Vec_PtrPush( pNtk->vLatches, pObj );
+ Vec_PtrPush( pNtk->vCis, pObj );
+ Vec_PtrPush( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_BOX:
+ break;
+ default:
+ assert(0);
+ break;
}
- else if ( Abc_ObjIsNet(pObj) )
- {
- pNtk->nNets++;
- }
- else if ( Abc_ObjIsPi(pObj) )
- {
- Vec_PtrPush( pNtk->vPis, pObj );
- Vec_PtrPush( pNtk->vCis, pObj );
- }
- else if ( Abc_ObjIsPo(pObj) )
- {
- Vec_PtrPush( pNtk->vPos, pObj );
- Vec_PtrPush( pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsLatch(pObj) )
- {
- Vec_PtrPush( pNtk->vLatches, pObj );
- Vec_PtrPush( pNtk->vCis, pObj );
- Vec_PtrPush( pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsAssert(pObj) )
- {
- Vec_PtrPush( pNtk->vAsserts, pObj );
- Vec_PtrPush( pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsBi(pObj) )
- {
- Vec_PtrPush( pNtk->vCis, pObj );
- }
- else if ( Abc_ObjIsBo(pObj) )
- {
- Vec_PtrPush( pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsBox(pObj) )
+ return pObj;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deletes the object from the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
+{
+ Abc_Ntk_t * pNtk = pObj->pNtk;
+ Vec_Ptr_t * vNodes;
+ int i;
+ // delete fanins and fanouts
+ assert( !Abc_ObjIsComplement(pObj) );
+ vNodes = Vec_PtrAlloc( 100 );
+ Abc_NodeCollectFanouts( pObj, vNodes );
+ for ( i = 0; i < vNodes->nSize; i++ )
+ Abc_ObjDeleteFanin( vNodes->pArray[i], pObj );
+ Abc_NodeCollectFanins( pObj, vNodes );
+ for ( i = 0; i < vNodes->nSize; i++ )
+ Abc_ObjDeleteFanin( pObj, vNodes->pArray[i] );
+ Vec_PtrFree( vNodes );
+ // remove from the list of objects
+ Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
+ 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)
{
- pNtk->nBoxes++;
- Vec_PtrPush( pNtk->vBoxes, pObj );
+ case ABC_OBJ_NONE:
+ assert(0);
+ break;
+ case ABC_OBJ_CONST1:
+ assert(0);
+ break;
+ case ABC_OBJ_PIO:
+ assert(0);
+ break;
+ case ABC_OBJ_PI:
+ Vec_PtrRemove( pNtk->vPis, pObj );
+ Vec_PtrRemove( pNtk->vCis, pObj );
+ break;
+ case ABC_OBJ_PO:
+ Vec_PtrRemove( pNtk->vPos, pObj );
+ Vec_PtrRemove( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_BI:
+ Vec_PtrRemove( pNtk->vCis, pObj );
+ break;
+ case ABC_OBJ_BO:
+ Vec_PtrRemove( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_ASSERT:
+ Vec_PtrRemove( pNtk->vAsserts, pObj );
+ Vec_PtrRemove( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_NET:
+ pObj->pData = NULL;
+ break;
+ case ABC_OBJ_NODE:
+ if ( Abc_NtkHasBdd(pNtk) )
+ Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+ pObj->pData = NULL;
+ break;
+ case ABC_OBJ_LATCH:
+ Vec_PtrRemove( pNtk->vLatches, pObj );
+ Vec_PtrRemove( pNtk->vCis, pObj );
+ Vec_PtrRemove( pNtk->vCos, pObj );
+ break;
+ case ABC_OBJ_BOX:
+ break;
+ default:
+ assert(0);
+ break;
}
- else assert( 0 );
+ // recycle the object memory
+ Abc_ObjRecycle( pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deletes the node and MFFC of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+{
+ Abc_Ntk_t * pNtk = pObj->pNtk;
+ Vec_Ptr_t * vNodes;
+ int i;
+ assert( !Abc_ObjIsComplement(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 );
+ Vec_PtrFree( vNodes );
}
/**Function*************************************************************
@@ -157,9 +287,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
{
Abc_Obj_t * pObjNew;
// create the new object
- pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
- // add the object to the network
- Abc_ObjAdd( pObjNew );
+ pObjNew = Abc_NtkObjAdd( pNtkNew, pObj->Type );
// copy functionality/names
if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible
{
@@ -203,132 +331,12 @@ Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pObj )
{
Abc_Obj_t * pClone, * pFanin;
int i;
- pClone = Abc_ObjAlloc( pObj->pNtk, pObj->Type );
- Abc_ObjAdd( pClone );
+ pClone = Abc_NtkObjAdd( pObj->pNtk, pObj->Type );
Abc_ObjForEachFanin( pObj, pFanin, i )
Abc_ObjAddFanin( pClone, pFanin );
return pClone;
}
-/**Function*************************************************************
-
- Synopsis [Deletes the object from the network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
-{
- Abc_Ntk_t * pNtk = pObj->pNtk;
- Vec_Ptr_t * vNodes;
- int i;
-
- assert( !Abc_ObjIsComplement(pObj) );
-
- // delete fanins and fanouts
- vNodes = Vec_PtrAlloc( 100 );
- Abc_NodeCollectFanouts( pObj, vNodes );
- for ( i = 0; i < vNodes->nSize; i++ )
- Abc_ObjDeleteFanin( vNodes->pArray[i], pObj );
- Abc_NodeCollectFanins( pObj, vNodes );
- for ( i = 0; i < vNodes->nSize; i++ )
- Abc_ObjDeleteFanin( pObj, vNodes->pArray[i] );
- Vec_PtrFree( vNodes );
-
- // remove from the list of objects
- Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
- pObj->Id = (1<<26)-1;
- 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
- if ( Abc_ObjIsNet(pObj) )
- {
- pObj->pData = NULL;
- pNtk->nNets--;
- }
- else if ( Abc_ObjIsNode(pObj) )
- {
- if ( Abc_NtkHasBdd(pNtk) )
- Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
- pObj->pData = NULL;
- pNtk->nNodes--;
- }
- else if ( Abc_ObjIsLatch(pObj) )
- {
- Vec_PtrRemove( pNtk->vLatches, pObj );
- Vec_PtrRemove( pNtk->vCis, pObj );
- Vec_PtrRemove( pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsPi(pObj) )
- {
- Vec_PtrRemove( pObj->pNtk->vPis, pObj );
- Vec_PtrRemove( pObj->pNtk->vCis, pObj );
- }
- else if ( Abc_ObjIsPo(pObj) )
- {
- Vec_PtrRemove( pObj->pNtk->vPos, pObj );
- Vec_PtrRemove( pObj->pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsBi(pObj) )
- {
- Vec_PtrRemove( pObj->pNtk->vCis, pObj );
- }
- else if ( Abc_ObjIsBo(pObj) )
- {
- Vec_PtrRemove( pObj->pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsAssert(pObj) )
- {
- Vec_PtrRemove( pObj->pNtk->vAsserts, pObj );
- Vec_PtrRemove( pObj->pNtk->vCos, pObj );
- }
- else if ( Abc_ObjIsBox(pObj) )
- {
- pNtk->nBoxes--;
- Vec_PtrRemove( pObj->pNtk->vBoxes, pObj );
- }
- else
- assert( 0 );
- // recycle the net itself
- Abc_ObjRecycle( pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Deletes the node and MFFC of the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
-{
- Abc_Ntk_t * pNtk = pObj->pNtk;
- Vec_Ptr_t * vNodes;
- int i;
- assert( !Abc_ObjIsComplement(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 );
- Vec_PtrFree( vNodes );
-}
-
/**Function*************************************************************
@@ -458,129 +466,13 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
{
Abc_Obj_t * pNet;
assert( Abc_NtkIsNetlist(pNtk) );
- if ( pNet = Abc_NtkFindNet( pNtk, pName ) )
+ if ( pName && (pNet = Abc_NtkFindNet( pNtk, pName )) )
return pNet;
// create a new net
- pNet = Abc_ObjAlloc( pNtk, ABC_OBJ_NET );
- Abc_ObjAdd( pNet );
- pNet->pData = Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL );
+ pNet = Abc_NtkObjAdd( pNtk, ABC_OBJ_NET );
+ pNet->pData = pName? Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL ) : NULL;
return pNet;
}
-
-/**Function*************************************************************
-
- Synopsis [Create node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_NODE );
- Abc_ObjAdd( pObj );
- return pObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Create multi-input/multi-output box.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateBox( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_BOX );
- Abc_ObjAdd( pObj );
- return pObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Create primary input.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_PI );
- Abc_ObjAdd( pObj );
- return pObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Create primary output.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_PO );
- Abc_ObjAdd( pObj );
- return pObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates latch.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_LATCH );
- pObj->pData = (void *)ABC_INIT_NONE;
- Abc_ObjAdd( pObj );
- return pObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates assert.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )
-{
- Abc_Obj_t * pObj;
- pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_ASSERT );
- Abc_ObjAdd( pObj );
- return pObj;
-}
/**Function*************************************************************
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index dfd49f6e..ff05fe69 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
assert( Abc_NtkIsStrash(pNtk2) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -304,7 +304,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -356,7 +356,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
assert( 1 == Abc_NtkCoNum(pNtk) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_miter", pNtk->pName );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -423,7 +423,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In
assert( In2 < Abc_NtkCiNum(pNtk) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) );
pNtkMiter->pName = Extra_UtilStrsav(Buffer);
@@ -488,7 +488,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
assert( In < Abc_NtkCiNum(pNtk) );
// start the new network
- pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) );
// get the root output
@@ -669,7 +669,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
assert( Abc_NtkIsStrash(pNtk) );
assert( Abc_NtkIsDfsOrdered(pNtk) );
// start the new network
- pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// create new latches (or their initial values) and remember them in the new latches
@@ -806,7 +806,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
assert( nFrames > 0 );
assert( Abc_NtkIsStrash(pNtk) );
// start the new network
- pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
pNtkFrames->pName = Extra_UtilStrsav(Buffer);
// create new latches (or their initial values) and remember them in the new latches
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 99ed5636..ac46501c 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -78,7 +78,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
return NULL;
// start the network
- pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+ pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
pNtk->pName = Extra_UtilStrsav(pNamePo);
// make sure the new manager has enough inputs
Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index cb1d2a38..e3bb764d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -66,7 +66,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
if ( Abc_NtkIsNetlist(pNtk) )
{
fprintf( pFile, " net = %5d", Abc_NtkNetNum(pNtk) );
- fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
+ fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
+ fprintf( pFile, " box = %5d", Abc_NtkBoxNum(pNtk) );
}
else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
{
@@ -83,7 +84,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
else
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
- if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
+ if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) || Abc_NtkIsNetlist(pNtk) )
{
}
else if ( Abc_NtkHasSop(pNtk) )
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 61bc8b09..03073075 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -676,7 +676,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
int i;
assert( Abc_NtkIsStrash(pNtk) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav( "temp" );
// map the constant nodes
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 86f13884..02bfca17 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -436,6 +436,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
int clk1 = clock(), clk;
int fOrderCiVarsFirst = 0;
int nLevelsMax = Abc_AigGetLevelNum(pNtk);
+ int RetValue = 0;
assert( Abc_NtkIsStrash(pNtk) );
@@ -481,7 +482,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
}
// add the trivial clause
if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
- return 0;
+ goto Quits;
}
// add the clauses
@@ -515,7 +516,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
}
// add the clauses
if ( !Abc_NtkClauseMux( pSat, pNode, pNodeC, pNodeT, pNodeE, vVars ) )
- return 0;
+ goto Quits;
}
else
{
@@ -537,12 +538,12 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
{
if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) )
// if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) )
- return 0;
+ goto Quits;
}
else
{
if ( !Abc_NtkClauseAnd( pSat, pNode, vSuper, vVars ) )
- return 0;
+ goto Quits;
}
}
// add the variables to the J-frontier
@@ -597,11 +598,13 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
Asat_SolverSetFactors( pSat, Vec_IntReleaseArray(vLevels) );
Vec_IntFree( vLevels );
*/
+ RetValue = 1;
+Quits :
// delete
Vec_IntFree( vVars );
Vec_PtrFree( vNodes );
Vec_PtrFree( vSuper );
- return 1;
+ return RetValue;
}
/**Function*************************************************************
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index c69aeabf..c54ea33c 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -250,7 +250,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
Abc_Obj_t * pFanin;
int i;
assert( Abc_ObjIsNode(pNodeOld) );
- assert( Abc_NtkIsAigLogic(pNodeOld->pNtk) );
+ assert( Abc_NtkHasAig(pNodeOld->pNtk) && !Abc_NtkIsStrash(pNodeOld->pNtk) );
// get the local AIG manager and the local root node
pMan = pNodeOld->pNtk->pManFunc;
pRoot = pNodeOld->pData;
@@ -317,7 +317,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
// get the cutoff level
LevelCut = ABC_MAX( 0, Abc_AigGetLevelNum(pNtk) - nLevels );
// start the network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew);
// create PIs below the cut and nodes above the cut
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index b5306bea..156d9b3d 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -284,7 +284,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
int i;
// start the new network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
pNtkNew->pName = Extra_UtilStrsav( "exdc" );
pNtkNew->pSpec = NULL;
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index 58d9f64e..50baa285 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -514,7 +514,7 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
if ( vCorresp )
Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL );
// start the new network
- pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
if ( fShortNames )
{
pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName);
@@ -719,7 +719,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
assert( Abc_NtkIsStrash(pNtk) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
pNtkNew->pName = Extra_UtilStrsav("exdc");
pNtkNew->pSpec = NULL;
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
index 29b5d3a6..339d64d1 100644
--- a/src/base/abci/abcVanImp.c
+++ b/src/base/abci/abcVanImp.c
@@ -877,7 +877,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
assert( Abc_NtkIsStrash(pNtk) );
// start the network
- pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+ pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
pNtkNew->pName = Extra_UtilStrsav( "exdc" );
pNtkNew->pSpec = NULL;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 0cc3c7d9..86e8845b 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -50,6 +50,8 @@ static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteVerLib ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
+extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -667,13 +669,13 @@ usage:
***********************************************************************/
int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Abc_Ntk_t * pNtk;
+ Abc_Ntk_t * pNtk, * pNtkNew;
Abc_Lib_t * pDesign;
char * FileName;
FILE * pFile;
int fCheck;
int c;
- extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
+ extern Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib );
fCheck = 1;
Extra_UtilGetoptReset();
@@ -709,21 +711,32 @@ int IoCommandReadVer( Abc_Frame_t * pAbc, int argc, char ** argv )
fclose( pFile );
// set the new network
- pDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck );
+ pDesign = Ver_ParseFile( FileName, Abc_FrameReadLibVer(), fCheck, 1 );
if ( pDesign == NULL )
{
fprintf( pAbc->Err, "Reading network from the verilog file has failed.\n" );
return 1;
}
+
// derive root design
pNtk = Abc_LibDeriveRoot( pDesign );
+ Abc_LibFree( pDesign );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Deriving root module has failed.\n" );
return 1;
}
+
+ // derive the AIG network from this design
+ pNtkNew = Abc_LibDeriveAig( pNtk, Abc_FrameReadLibVer() );
+ Abc_NtkDelete( pNtk );
+ if ( pNtkNew == NULL )
+ {
+ fprintf( pAbc->Err, "Converting root module to AIG has failed.\n" );
+ return 1;
+ }
// replace the current network
- Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
return 0;
usage:
@@ -753,7 +766,6 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pFile;
int fCheck;
int c;
- extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
fCheck = 1;
Extra_UtilGetoptReset();
@@ -789,7 +801,7 @@ int IoCommandReadVerLib( Abc_Frame_t * pAbc, int argc, char ** argv )
fclose( pFile );
// set the new network
- pLibrary = Ver_ParseFile( FileName, NULL, fCheck );
+ pLibrary = Ver_ParseFile( FileName, NULL, fCheck, 0 );
if ( pLibrary == NULL )
{
fprintf( pAbc->Err, "Reading library from the verilog file has failed.\n" );
@@ -1613,7 +1625,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
fprintf( pAbc->Out, "Writing PLA has failed.\n" );
return 0;
}
- Io_WriteVerilog( pNtkTemp, FileName );
+ Io_WriteVerilog( pNtkTemp, FileName, 0 );
Abc_NtkDelete( pNtkTemp );
return 0;
@@ -1638,10 +1650,10 @@ usage:
***********************************************************************/
int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
{
- st_table * tLibrary;
+ Abc_Lib_t * pLibrary;
char * FileName;
int c;
- extern void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName );
+ extern void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
@@ -1663,13 +1675,13 @@ int IoCommandWriteVerLib( Abc_Frame_t * pAbc, int argc, char **argv )
FileName = argv[globalUtilOptind];
// derive the netlist
- tLibrary = Abc_FrameReadLibVer();
- if ( tLibrary == NULL )
+ pLibrary = Abc_FrameReadLibVer();
+ if ( pLibrary == NULL )
{
fprintf( pAbc->Out, "Verilog library is not specified.\n" );
return 0;
}
- Io_WriteVerilogLibrary( tLibrary, FileName );
+ Io_WriteVerilogLibrary( pLibrary, FileName );
return 0;
usage:
@@ -1741,7 +1753,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
int i;
if ( pFile == NULL )
{
- fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName );
+ fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", FileName );
return 1;
}
if ( fNames )
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 8c8d6bed..c42d2016 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -97,7 +97,7 @@ extern void Io_WriteList( Abc_Ntk_t * pNtk, char * pFileName, int
/*=== abcWritePla.c ==========================================================*/
extern int Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
/*=== abcWriteVerilog.c ==========================================================*/
-extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
+extern void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName, int fVerLibStyle );
#ifdef __cplusplus
}
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 83b642a0..367d693b 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -73,7 +73,7 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
nAnds = atoi( pCur ); while ( *pCur++ );
// allocate the empty AIG
- pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
pNtkNew->pName = Extra_UtilStrsav( pName );
pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index ade9051f..5d6bc2f1 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -211,7 +211,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
assert( p->vTokens != NULL );
// create the new network
- p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+ p->pNtkCur = pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
// read the model name
if ( strcmp( p->vTokens->pArray[0], ".model" ) == 0 )
pNtk->pName = Extra_UtilStrsav( p->vTokens->pArray[1] );
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index a4610cac..4550d286 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -271,7 +271,7 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p )
pModelName = vTokens->pArray[1];
// allocate the empty network
- pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP );
+ pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP, 1 );
pNtk->pName = Extra_UtilStrsav( pModelName );
pNtk->pSpec = Extra_UtilStrsav( p->pFileName );
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
index 594bf4eb..2234b3a3 100644
--- a/src/base/io/ioWriteVer.c
+++ b/src/base/io/ioWriteVer.c
@@ -26,7 +26,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle );
static void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
static void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
@@ -34,6 +34,7 @@ static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_WriteVerilogVerLibStyle( FILE * pFile, Abc_Ntk_t * pNtk );
static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
@@ -53,7 +54,7 @@ static int Io_WriteVerilogWiresCount( Abc_Ntk_t * pNtk );
SeeAlso []
***********************************************************************/
-void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
+void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName, int fVerLibStyle )
{
FILE * pFile;
@@ -75,7 +76,7 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
// write the equations for the network
fprintf( pFile, "// Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
- Io_WriteVerilogInt( pFile, pNtk );
+ Io_WriteVerilogInt( pFile, pNtk, fVerLibStyle );
fprintf( pFile, "\n" );
fclose( pFile );
}
@@ -91,12 +92,11 @@ void Io_WriteVerilog( Abc_Ntk_t * pNtk, char * pFileName )
SeeAlso []
***********************************************************************/
-void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
+void Io_WriteVerilogLibrary( Abc_Lib_t * pLibrary, char * pFileName )
{
FILE * pFile;
- st_generator * gen;
Abc_Ntk_t * pNtk, * pNetlist;
- char * pName;
+ int i;
// start the output stream
pFile = fopen( pFileName, "w" );
@@ -109,15 +109,17 @@ void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
fprintf( pFile, "// Verilog library \"%s\" written by ABC on %s\n", pFileName, Extra_TimeStamp() );
fprintf( pFile, "\n" );
// write modules
- st_foreach_item( tLibrary, gen, (char**)&pName, (char**)&pNtk )
+ Vec_PtrForEachEntry( pLibrary->vModules, pNtk, i )
{
// create netlist
- pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+// pNetlist = Abc_NtkLogicToNetlist( pNtk, 0 );
+ assert( Abc_NtkIsNetlist(pNtk) );
+ pNetlist = pNtk;
// write the equations for the network
- Io_WriteVerilogInt( pFile, pNetlist );
+ Io_WriteVerilogInt( pFile, pNetlist, 1 );
fprintf( pFile, "\n" );
// delete the netlist
- Abc_NtkDelete( pNetlist );
+// Abc_NtkDelete( pNetlist );
}
fclose( pFile );
@@ -134,7 +136,7 @@ void Io_WriteVerilogLibrary( st_table * tLibrary, char * pFileName )
SeeAlso []
***********************************************************************/
-void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk, int fVerLibStyle )
{
// write inputs and outputs
fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) );
@@ -161,8 +163,10 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
Io_WriteVerilogWires( pFile, pNtk, 4 );
fprintf( pFile, ";\n" );
}
- // write the nodes
- if ( Abc_NtkHasMapping(pNtk) )
+ // write nodes
+ if ( fVerLibStyle )
+ Io_WriteVerilogVerLibStyle( pFile, pNtk );
+ else if ( Abc_NtkHasMapping(pNtk) )
Io_WriteVerilogGates( pFile, pNtk );
else
Io_WriteVerilogNodes( pFile, pNtk );
@@ -438,6 +442,65 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Writes the nodes and boxes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteVerilogVerLibStyle( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+ Vec_Vec_t * vLevels;
+ Abc_Ntk_t * pNtkGate;
+ Abc_Obj_t * pObj, * pTerm, * pFanin;
+ Aig_Obj_t * pFunc;
+ int i, k, Counter, nDigits;
+
+ Counter = 1;
+ nDigits = Extra_Base10Log( Abc_NtkNodeNum(pNtk) );
+
+ // write boxes
+ Abc_NtkForEachBox( pNtk, pObj, i )
+ {
+ pNtkGate = pObj->pData;
+ fprintf( pFile, " %s g%0*d", pNtkGate->pName, nDigits, Counter++ );
+ fprintf( pFile, "(" );
+ Abc_NtkForEachPi( pNtkGate, pTerm, k )
+ {
+ fprintf( pFile, ".%s ", Io_WriteVerilogGetName(Abc_ObjFanout0(pTerm)) );
+ fprintf( pFile, "(%s), ", Io_WriteVerilogGetName(Abc_ObjFanin(pObj,k)) );
+ }
+ Abc_NtkForEachPo( pNtkGate, pTerm, k )
+ {
+ fprintf( pFile, ".%s ", Io_WriteVerilogGetName(Abc_ObjFanin0(pTerm)) );
+ fprintf( pFile, "(%s)%s", Io_WriteVerilogGetName(Abc_ObjFanout(pObj,k)), k==Abc_NtkPoNum(pNtkGate)-1? "":", " );
+ }
+ fprintf( pFile, ");\n" );
+ }
+ // write nodes
+ vLevels = Vec_VecAlloc( 10 );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ pFunc = pObj->pData;
+ fprintf( pFile, " assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+ // set the input names
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Aig_IthVar(pNtk->pManFunc, k)->pData = Extra_UtilStrsav(Io_WriteVerilogGetName(pFanin));
+ // write the formula
+ Aig_ObjPrintVerilog( pFile, pFunc, vLevels, 0 );
+ fprintf( pFile, ";\n" );
+ // clear the input names
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ free( Aig_IthVar(pNtk->pManFunc, k)->pData );
+ }
+ Vec_VecFree( vLevels );
+}
+
+/**Function*************************************************************
+
Synopsis [Writes the gates.]
Description []
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 358d306c..21215af6 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -303,7 +303,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
// create the network for the initial state computation
// start the table and the array of PO values
- pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+ pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
tTable = stmm_init_table( stmm_numcmp, stmm_numhash );
vValues = Vec_IntAlloc( 100 );
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index 30a21086..8dc29855 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
// start the network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
@@ -109,7 +109,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
Vec_PtrWriteEntry( pNtkNew->vObjs, pObj->pCopy->Id, pObj->pCopy );
pNtkNew->nObjs++;
}
- pNtkNew->nNodes = pNtk->nNodes;
+ pNtkNew->nObjCounts[ABC_OBJ_NODE] = pNtk->nObjCounts[ABC_OBJ_NODE];
// create PI/PO and their names
Abc_NtkForEachPi( pNtk, pObj, i )
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 080abcb2..1945826f 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -116,7 +116,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
}
// start the network
- pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
+ pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
diff --git a/src/misc/extra/extraUtilMemory.c b/src/misc/extra/extraUtilMemory.c
index 768f86fa..bc58527b 100644
--- a/src/misc/extra/extraUtilMemory.c
+++ b/src/misc/extra/extraUtilMemory.c
@@ -322,7 +322,7 @@ Extra_MmFlex_t * Extra_MmFlexStart()
p->pCurrent = NULL;
p->pEnd = NULL;
- p->nChunkSize = (1 << 12);
+ p->nChunkSize = (1 << 10);
p->nChunksAlloc = 64;
p->nChunks = 0;
p->pChunks = ALLOC( char *, p->nChunksAlloc );
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 4a97fc91..1973bd46 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -494,14 +494,18 @@ static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int
if ( p->nSize == 0 )
p->nCap = 1;
- pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
-// pArray = ALLOC( int, p->nCap * 2 );
+ if ( pMemMan )
+ pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
+ else
+ pArray = ALLOC( int, p->nCap * 2 );
if ( p->pArray )
{
for ( i = 0; i < p->nSize; i++ )
pArray[i] = p->pArray[i];
- Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
-// free( p->pArray );
+ if ( pMemMan )
+ Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
+ else
+ free( p->pArray );
}
p->nCap *= 2;
p->pArray = pArray;
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 353f6c4c..75ceab4b 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -79,7 +79,7 @@ ABC_Manager ABC_InitManager()
Abc_Start();
mng = ALLOC( ABC_Manager_t, 1 );
memset( mng, 0, sizeof(ABC_Manager_t) );
- mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+ mng->pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
mng->pNtk->pName = Extra_UtilStrsav("csat_network");
mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
diff --git a/src/temp/aig/aig.h b/src/temp/aig/aig.h
index e3e35b0c..e489d978 100644
--- a/src/temp/aig/aig.h
+++ b/src/temp/aig/aig.h
@@ -290,9 +290,11 @@ extern void Aig_TableProfile( Aig_Man_t * p );
/*=== aigUtil.c =========================================================*/
extern void Aig_ManIncrementTravId( Aig_Man_t * p );
extern void Aig_ManCleanData( Aig_Man_t * p );
-extern int Aig_ObjMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode );
+extern void Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
extern int Aig_ObjIsMuxType( Aig_Obj_t * pObj );
+extern int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
extern Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
+extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
diff --git a/src/temp/aig/aigUtil.c b/src/temp/aig/aigUtil.c
index eb93cba1..99966e7d 100644
--- a/src/temp/aig/aigUtil.c
+++ b/src/temp/aig/aigUtil.c
@@ -73,6 +73,46 @@ void Aig_ManCleanData( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Detects multi-input gate rooted at this node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ObjCollectMulti_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+ if ( pRoot != pObj && (Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjType(pRoot) != Aig_ObjType(pObj)) )
+ {
+ Vec_PtrPushUnique(vSuper, pObj);
+ return;
+ }
+ Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
+ Aig_ObjCollectMulti_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects multi-input gate rooted at this node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ObjCollectMulti( Aig_Obj_t * pRoot, Vec_Ptr_t * vSuper )
+{
+ assert( !Aig_IsComplement(pRoot) );
+ Vec_PtrClear( vSuper );
+ Aig_ObjCollectMulti_rec( pRoot, pRoot, vSuper );
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
Description []
@@ -106,6 +146,48 @@ int Aig_ObjIsMuxType( Aig_Obj_t * pNode )
(Aig_ObjFanin1(pNode0) == Aig_ObjFanin1(pNode1) && (Aig_ObjFaninC1(pNode0) ^ Aig_ObjFaninC1(pNode1)));
}
+
+/**Function*************************************************************
+
+ Synopsis [Recognizes what nodes are inputs of the EXOR.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 )
+{
+ Aig_Obj_t * p0, * p1;
+ assert( !Aig_IsComplement(pObj) );
+ if ( !Aig_ObjIsNode(pObj) )
+ return 0;
+ if ( Aig_ObjIsExor(pObj) )
+ {
+ *ppFan0 = Aig_ObjChild0(pObj);
+ *ppFan1 = Aig_ObjChild1(pObj);
+ return 1;
+ }
+ assert( Aig_ObjIsAnd(pObj) );
+ p0 = Aig_ObjChild0(pObj);
+ p1 = Aig_ObjChild1(pObj);
+ if ( !Aig_IsComplement(p0) || !Aig_IsComplement(p1) )
+ return 0;
+ p0 = Aig_Regular(p0);
+ p1 = Aig_Regular(p1);
+ if ( !Aig_ObjIsAnd(p0) || !Aig_ObjIsAnd(p1) )
+ return 0;
+ if ( Aig_ObjFanin0(p0) != Aig_ObjFanin0(p1) || Aig_ObjFanin1(p0) != Aig_ObjFanin1(p1) )
+ return 0;
+ if ( Aig_ObjFaninC0(p0) == Aig_ObjFaninC0(p1) || Aig_ObjFaninC1(p0) == Aig_ObjFaninC1(p1) )
+ return 0;
+ *ppFan0 = Aig_ObjChild0(p0);
+ *ppFan1 = Aig_ObjChild1(p0);
+ return 1;
+}
+
/**Function*************************************************************
Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
@@ -198,6 +280,95 @@ Aig_Obj_t * Aig_ObjRecognizeMux( Aig_Obj_t * pNode, Aig_Obj_t ** ppNodeT, Aig_Ob
return NULL;
}
+
+/**Function*************************************************************
+
+ Synopsis [Prints Verilog formula for the AIG rooted at this node.]
+
+ Description [The formula is in terms of PIs, which should have
+ their names assigned in pObj->pData fields.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
+{
+ Vec_Ptr_t * vSuper;
+ Aig_Obj_t * pFanin, * pFanin0, * pFanin1, * pFaninC;
+ int fCompl, i;
+ // store the complemented attribute
+ fCompl = Aig_IsComplement(pObj);
+ pObj = Aig_Regular(pObj);
+ // constant case
+ if ( Aig_ObjIsConst1(pObj) )
+ {
+ fprintf( pFile, "%d", !fCompl );
+ return;
+ }
+ // PI case
+ if ( Aig_ObjIsPi(pObj) )
+ {
+ fprintf( pFile, "%s%s", fCompl? "~" : "", pObj->pData );
+ return;
+ }
+ // EXOR case
+ if ( Aig_ObjIsExor(pObj) )
+ {
+ Vec_VecExpand( vLevels, Level );
+ vSuper = Vec_VecEntry( vLevels, Level );
+ Aig_ObjCollectMulti( pObj, vSuper );
+ fprintf( pFile, "%s", (Level==0? "" : "(") );
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ {
+ Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
+ if ( i < Vec_PtrSize(vSuper) - 1 )
+ fprintf( pFile, " ^ " );
+ }
+ fprintf( pFile, "%s", (Level==0? "" : ")") );
+ return;
+ }
+ // MUX case
+ if ( Aig_ObjIsMuxType(pObj) )
+ {
+ if ( Aig_ObjRecognizeExor( pObj, &pFanin0, &pFanin1 ) )
+ {
+ fprintf( pFile, "%s", (Level==0? "" : "(") );
+ Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
+ fprintf( pFile, " ^ " );
+ Aig_ObjPrintVerilog( pFile, pFanin1, vLevels, Level+1 );
+ fprintf( pFile, "%s", (Level==0? "" : ")") );
+ }
+ else
+ {
+ pFaninC = Aig_ObjRecognizeMux( pObj, &pFanin1, &pFanin0 );
+ fprintf( pFile, "%s", (Level==0? "" : "(") );
+ Aig_ObjPrintVerilog( pFile, pFaninC, vLevels, Level+1 );
+ fprintf( pFile, " ? " );
+ Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin1, fCompl), vLevels, Level+1 );
+ fprintf( pFile, " : " );
+ Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin0, fCompl), vLevels, Level+1 );
+ fprintf( pFile, "%s", (Level==0? "" : ")") );
+ }
+ return;
+ }
+ // AND case
+ Vec_VecExpand( vLevels, Level );
+ vSuper = Vec_VecEntry(vLevels, Level);
+ Aig_ObjCollectMulti( pObj, vSuper );
+ fprintf( pFile, "%s", (Level==0? "" : "(") );
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ {
+ Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
+ if ( i < Vec_PtrSize(vSuper) - 1 )
+ fprintf( pFile, " %s ", fCompl? "|" : "&" );
+ }
+ fprintf( pFile, "%s", (Level==0? "" : ")") );
+ return;
+}
+
+
/**Function*************************************************************
Synopsis [Prints node in HAIG.]
@@ -250,6 +421,8 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
printf( "\n" );
}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/temp/ver/ver.h b/src/temp/ver/ver.h
index 3e351840..c7c18f79 100644
--- a/src/temp/ver/ver.h
+++ b/src/temp/ver/ver.h
@@ -52,7 +52,9 @@ struct Ver_Man_t_
// current network and library
Abc_Ntk_t * pNtkCur; // the network under construction
Abc_Lib_t * pDesign; // the current design
- Abc_Lib_t * pGateLib; // the current technology library
+ // parameters
+ int fUseMemMan; // allocate memory manager in the networks
+ int fCheck; // checks network for currectness
// error recovery
FILE * Output;
int fTopLevel;
@@ -77,10 +79,11 @@ struct Ver_Man_t_
////////////////////////////////////////////////////////////////////////
/*=== verCore.c ========================================================*/
-extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck );
+extern Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan );
extern void Ver_ParsePrintErrorMessage( Ver_Man_t * p );
/*=== verFormula.c ========================================================*/
extern void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_Ptr_t * vStackFn, Vec_Int_t * vStackOp, char * pErrorMessage );
+extern void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage );
/*=== verParse.c ========================================================*/
extern int Ver_ParseSkipComments( Ver_Man_t * p );
extern char * Ver_ParseGetName( Ver_Man_t * p );
diff --git a/src/temp/ver/verCore.c b/src/temp/ver/verCore.c
index e868c4e3..99311c98 100644
--- a/src/temp/ver/verCore.c
+++ b/src/temp/ver/verCore.c
@@ -37,7 +37,7 @@ typedef enum {
static Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib );
static void Ver_ParseStop( Ver_Man_t * p );
static void Ver_ParseFreeData( Ver_Man_t * p );
-static void Ver_ParseInternal( Ver_Man_t * p, int fCheck );
+static void Ver_ParseInternal( Ver_Man_t * p );
static int Ver_ParseModule( Ver_Man_t * p );
static int Ver_ParseSignal( Ver_Man_t * p, Ver_SignalType_t SigType );
static int Ver_ParseAssign( Ver_Man_t * p );
@@ -64,14 +64,16 @@ static Abc_Obj_t * Ver_ParseCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char *
SeeAlso []
***********************************************************************/
-Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck )
+Abc_Lib_t * Ver_ParseFile( char * pFileName, Abc_Lib_t * pGateLib, int fCheck, int fUseMemMan )
{
Ver_Man_t * p;
Abc_Lib_t * pDesign;
// start the parser
p = Ver_ParseStart( pFileName, pGateLib );
+ p->fCheck = fCheck;
+ p->fUseMemMan = fUseMemMan;
// parse the file
- Ver_ParseInternal( p, fCheck );
+ Ver_ParseInternal( p );
// save the result
pDesign = p->pDesign;
p->pDesign = NULL;
@@ -98,13 +100,14 @@ Ver_Man_t * Ver_ParseStart( char * pFileName, Abc_Lib_t * pGateLib )
memset( p, 0, sizeof(Ver_Man_t) );
p->pFileName = pFileName;
p->pReader = Ver_StreamAlloc( pFileName );
- p->pDesign = Abc_LibCreate( pFileName );
- p->pGateLib = pGateLib;
p->Output = stdout;
p->pProgress = Extra_ProgressBarStart( stdout, Ver_StreamGetFileSize(p->pReader) );
p->vNames = Vec_PtrAlloc( 100 );
p->vStackFn = Vec_PtrAlloc( 100 );
p->vStackOp = Vec_IntAlloc( 100 );
+ // create the design library and assign the technology library
+ p->pDesign = Abc_LibCreate( pFileName );
+ p->pDesign->pLibrary = pGateLib;
return p;
}
@@ -141,7 +144,7 @@ void Ver_ParseStop( Ver_Man_t * p )
SeeAlso []
***********************************************************************/
-void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck )
+void Ver_ParseInternal( Ver_Man_t * pMan )
{
char * pToken;
while ( 1 )
@@ -162,7 +165,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck )
return;
// check the network for correctness
- if ( fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) )
+ if ( pMan->fCheck && !Abc_NtkCheckRead( pMan->pNtkCur ) )
{
pMan->fTopLevel = 1;
sprintf( pMan->sError, "The network check has failed.", pMan->pNtkCur->pName );
@@ -177,6 +180,7 @@ void Ver_ParseInternal( Ver_Man_t * pMan, int fCheck )
Ver_ParsePrintErrorMessage( pMan );
return;
}
+ Vec_PtrPush( pMan->pDesign->vModules, pMan->pNtkCur );
st_insert( pMan->pDesign->tModules, pMan->pNtkCur->pName, (char *)pMan->pNtkCur );
pMan->pNtkCur = NULL;
}
@@ -253,23 +257,19 @@ int Ver_ParseModule( Ver_Man_t * pMan )
// start the current network
assert( pMan->pNtkCur == NULL );
- pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX );
-
- pNtk->ntkFunc = ABC_FUNC_AIG;
- assert( pNtk->pManFunc == NULL );
+ pNtk = pMan->pNtkCur = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_BLACKBOX, pMan->fUseMemMan );
+ pNtk->ntkFunc = ABC_FUNC_AIG;
pNtk->pManFunc = pMan->pDesign->pManFunc;
// get the network name
pWord = Ver_ParseGetName( pMan );
pNtk->pName = Extra_UtilStrsav( pWord );
pNtk->pSpec = NULL;
-/*
- // create constant nodes and nets
- pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
- Abc_ObjAddFanin( pNet, xxxx AigAbc_AigConst1(pNtk) );
- pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
- Abc_ObjAddFanin( pNet, Abc_AigConst1(pNtk) );
-*/
+
+ // create constant nets
+ Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
+ Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
+
// make sure we stopped at the opening paranthesis
if ( Ver_StreamScanChar(p) != '(' )
{
@@ -281,6 +281,7 @@ int Ver_ParseModule( Ver_Man_t * pMan )
// skip to the end of parantheses
while ( 1 )
{
+ Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
Ver_StreamSkipToChars( p, ",/)" );
while ( Ver_StreamScanChar(p) == '/' )
{
@@ -299,6 +300,7 @@ int Ver_ParseModule( Ver_Man_t * pMan )
// parse the inputs/outputs/registers/wires/inouts
while ( 1 )
{
+ Extra_ProgressBarUpdate( pMan->pProgress, Ver_StreamGetCurPosition(p), NULL );
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
@@ -329,12 +331,8 @@ int Ver_ParseModule( Ver_Man_t * pMan )
else if ( !strcmp( pWord, "initial" ) )
RetValue = Ver_ParseInitial( pMan );
else if ( !strcmp( pWord, "endmodule" ) )
- {
- // if nothing is known, set the functionality to be black box
- Abc_NtkFinalizeRead( pNtk );
break;
- }
- else if ( pMan->pGateLib && st_lookup(pMan->pGateLib->tModules, pWord, (char**)&pNtkTemp) ) // gate library
+ else if ( pMan->pDesign->pLibrary && st_lookup(pMan->pDesign->pLibrary->tModules, pWord, (char**)&pNtkTemp) ) // gate library
RetValue = Ver_ParseGate( pMan, pNtkTemp );
else if ( pMan->pDesign && st_lookup(pMan->pDesign->tModules, pWord, (char**)&pNtkTemp) ) // current design
RetValue = Ver_ParseGate( pMan, pNtkTemp );
@@ -355,6 +353,22 @@ int Ver_ParseModule( Ver_Man_t * pMan )
if ( pWord == NULL )
return 0;
}
+
+ // check if constant 0 net is used
+ pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b0" );
+ if ( Abc_ObjFanoutNum(pNet) == 0 )
+ Abc_NtkDeleteObj(pNet);
+ else
+ Abc_ObjAddFanin( pNet, Abc_NodeCreateConst0(pNtk) );
+ // check if constant 1 net is used
+ pNet = Abc_NtkFindOrCreateNet( pNtk, "1'b1" );
+ if ( Abc_ObjFanoutNum(pNet) == 0 )
+ Abc_NtkDeleteObj(pNet);
+ else
+ Abc_ObjAddFanin( pNet, Abc_NodeCreateConst1(pNtk) );
+
+ // fix the dangling nets
+ Abc_NtkFinalizeRead( pNtk );
return 1;
}
@@ -415,29 +429,46 @@ int Ver_ParseAssign( Ver_Man_t * pMan )
Abc_Ntk_t * pNtk = pMan->pNtkCur;
Abc_Obj_t * pNode, * pNet;
char * pWord, * pName, * pEquation;
- DdNode * bFunc;
+ Aig_Obj_t * pFunc;
char Symbol;
- int i, Length;
+ int i, Length, fReduction;
// convert from the mapped netlist into the BDD netlist
if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
{
- pNtk->ntkFunc = ABC_FUNC_BDD;
- pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ pNtk->ntkFunc = ABC_FUNC_AIG;
+ assert( pNtk->pManFunc == NULL );
+ pNtk->pManFunc = pMan->pDesign->pManFunc;
}
- else if ( pNtk->ntkFunc != ABC_FUNC_BDD )
+ else if ( pNtk->ntkFunc != ABC_FUNC_AIG )
{
sprintf( pMan->sError, "The network %s appears to mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
+
while ( 1 )
{
// get the name of the output signal
pWord = Ver_ParseGetName( pMan );
if ( pWord == NULL )
return 0;
+ // consider the case of reduction operations
+ fReduction = (pWord[0] == '{');
+ if ( fReduction )
+ {
+ pWord++;
+ pWord[strlen(pWord)-1] = 0;
+ }
+ // get the fanout net
+ pNet = Abc_NtkFindNet( pNtk, pWord );
+ if ( pNet == NULL )
+ {
+ sprintf( pMan->sError, "Cannot read the assign statement for %s (output wire is not defined).", pWord );
+ Ver_ParsePrintErrorMessage( pMan );
+ return 0;
+ }
// get the fanout net
pNet = Abc_NtkFindNet( pNtk, pWord );
if ( pNet == NULL )
@@ -457,21 +488,27 @@ int Ver_ParseAssign( Ver_Man_t * pMan )
if ( !Ver_ParseSkipComments( pMan ) )
return 0;
// get the second name
- pEquation = Ver_StreamGetWord( p, ",;" );
+ if ( fReduction )
+ pEquation = Ver_StreamGetWord( p, ";" );
+ else
+ pEquation = Ver_StreamGetWord( p, ",;" );
if ( pEquation == NULL )
return 0;
// parse the formula
- bFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
- if ( bFunc == NULL )
+ if ( fReduction )
+ pFunc = Ver_FormulaReduction( pEquation, pNtk->pManFunc, pMan->vNames, pMan->sError );
+ else
+ pFunc = Ver_FormulaParser( pEquation, pNtk->pManFunc, pMan->vNames, pMan->vStackFn, pMan->vStackOp, pMan->sError );
+ if ( pFunc == NULL )
{
Ver_ParsePrintErrorMessage( pMan );
return 0;
}
- Cudd_Ref( bFunc );
+
// create the node with the given inputs
pNode = Abc_NtkCreateNode( pMan->pNtkCur );
- pNode->pData = bFunc;
+ pNode->pData = pFunc;
Abc_ObjAddFanin( pNet, pNode );
// connect to fanin nets
for ( i = 0; i < Vec_PtrSize(pMan->vNames)/2; i++ )
@@ -677,20 +714,8 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
Abc_Obj_t * pNetFormal, * pNetActual;
Abc_Obj_t * pObj, * pNode;
char * pWord, Symbol;
- int i, fCompl;
-
- // convert from the mapped netlist into the BDD netlist
- if ( pNtk->ntkFunc == ABC_FUNC_BLACKBOX )
- {
- pNtk->ntkFunc = ABC_FUNC_MAP;
- pNtk->pManFunc = pMan->pGateLib;
- }
- else if ( pNtk->ntkFunc != ABC_FUNC_MAP )
- {
- sprintf( pMan->sError, "The network %s appears to contain both mapped gates and assign statements. Currently such network are not allowed. One way to fix this problem is to replace assigns by buffers from the library.", pMan->pNtkCur );
- Ver_ParsePrintErrorMessage( pMan );
- return 0;
- }
+ int i, fCompl, fComplUsed = 0;
+ unsigned * pPolarity;
// clean the PI/PO pointers
Abc_NtkForEachPi( pNtkGate, pObj, i )
@@ -750,7 +775,12 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
// check if the name is complemented
fCompl = (pWord[0] == '~');
if ( fCompl )
+ {
+ fComplUsed = 1;
pWord++;
+ if ( pMan->pNtkCur->pData == NULL )
+ pMan->pNtkCur->pData = Extra_MmFlexStart();
+ }
// get the actual net
pNetActual = Abc_NtkFindNet( pMan->pNtkCur, pWord );
if ( pNetActual == NULL )
@@ -769,8 +799,8 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
}
// process the pair
- if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net
- Abc_ObjFanin0Ntk(pNetFormal)->pCopy = pNetActual; // Abc_ObjNotCond( pNetActual, fCompl );
+ if ( Abc_ObjIsPi(Abc_ObjFanin0Ntk(pNetFormal)) ) // PI net (with polarity!)
+ Abc_ObjFanin0Ntk(pNetFormal)->pCopy = Abc_ObjNotCond( pNetActual, fCompl );
else if ( Abc_ObjIsPo(Abc_ObjFanout0Ntk(pNetFormal)) ) // P0 net
{
assert( fCompl == 0 );
@@ -825,17 +855,38 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtkGate )
return 0;
}
*/
- // create a new node
- pNode = Abc_NtkCreateNode( pMan->pNtkCur );
+
+ // allocate memory to remember the phase
+ pPolarity = NULL;
+ if ( fComplUsed )
+ {
+ int nBytes = 4 * Abc_BitWordNum( Abc_NtkPiNum(pNtkGate) );
+ pPolarity = (unsigned *)Extra_MmFlexEntryFetch( pMan->pNtkCur->pData, nBytes );
+ memset( pPolarity, 0, nBytes );
+ }
+ // create box to represent this gate
+ pNode = Abc_NtkCreateBox( pMan->pNtkCur );
+ pNode->pNext = (Abc_Obj_t *)pPolarity;
+ pNode->pData = pNtkGate;
// connect to fanin nets
Abc_NtkForEachPi( pNtkGate, pObj, i )
+ {
+ if ( pPolarity && Abc_ObjIsComplement(pObj->pCopy) )
+ {
+ Abc_InfoSetBit( pPolarity, i );
+ pObj->pCopy = Abc_ObjRegular( pObj->pCopy );
+ }
+ assert( !Abc_ObjIsComplement(pObj->pCopy) );
Abc_ObjAddFanin( pNode, pObj->pCopy );
+ }
// connect to fanout nets
Abc_NtkForEachPo( pNtkGate, pObj, i )
+ {
if ( pObj->pCopy )
Abc_ObjAddFanin( pObj->pCopy, pNode );
- // set the functionality
- pNode->pData = pNtkGate;
+ else
+ Abc_ObjAddFanin( Abc_NtkFindOrCreateNet(pNtk, NULL), pNode );
+ }
return 1;
}
diff --git a/src/temp/ver/verFormula.c b/src/temp/ver/verFormula.c
index cfeb3e5f..2c2881c0 100644
--- a/src/temp/ver/verFormula.c
+++ b/src/temp/ver/verFormula.c
@@ -277,7 +277,7 @@ void * Ver_FormulaParser( char * pFormula, void * pMan, Vec_Ptr_t * vNames, Vec_
break;
}
Oper2 = Vec_IntPop( vStackOp ); // the operation before the last one
- if ( Oper2 >= Oper1 )
+ if ( Oper2 >= Oper1 && !(Oper1 == Oper2 && Oper1 == VER_PARSE_OPER_MUX) )
{ // if Oper2 precedence is higher or equal, execute it
if ( Ver_FormulaParserTopOper( pMan, vStackFn, Oper2 ) == NULL )
{
@@ -378,7 +378,7 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
int nLength, nLength2, i;
// find the end of the string delimited by other characters
pTemp = pString;
- while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' &&
+ while ( *pTemp && *pTemp != ' ' && *pTemp != '\t' && *pTemp != '\r' && *pTemp != '\n' && *pTemp != ',' && *pTemp != '}' &&
*pTemp != VER_PARSE_SYM_OPEN && *pTemp != VER_PARSE_SYM_CLOSE &&
*pTemp != VER_PARSE_SYM_NEGBEF1 && *pTemp != VER_PARSE_SYM_NEGBEF2 &&
*pTemp != VER_PARSE_SYM_AND && *pTemp != VER_PARSE_SYM_OR && *pTemp != VER_PARSE_SYM_XOR &&
@@ -402,6 +402,55 @@ int Ver_FormulaParserFindVar( char * pString, Vec_Ptr_t * vNames )
return i;
}
+/**Function*************************************************************
+
+ Synopsis [Returns the AIG representation of the reduction formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Ver_FormulaReduction( char * pFormula, void * pMan, Vec_Ptr_t * vNames, char * pErrorMessage )
+{
+ Aig_Obj_t * pRes;
+ int v, fCompl;
+ char Symbol;
+
+ // get the operation
+ Symbol = *pFormula++;
+ fCompl = ( Symbol == '~' );
+ if ( fCompl )
+ Symbol = *pFormula++;
+ // check the operation
+ if ( Symbol != '&' && Symbol != '|' && Symbol != '^' )
+ {
+ sprintf( pErrorMessage, "Ver_FormulaReduction(): Unknown operation (%c)\n", Symbol );
+ return NULL;
+ }
+ // skip the brace
+ while ( *pFormula++ != '{' );
+ // parse the names
+ Vec_PtrClear( vNames );
+ while ( *pFormula != '}' )
+ {
+ v = Ver_FormulaParserFindVar( pFormula, vNames );
+ pFormula += (int)Vec_PtrEntry( vNames, 2*v );
+ while ( *pFormula == ' ' || *pFormula == ',' )
+ pFormula++;
+ }
+ // compute the function
+ if ( Symbol == '&' )
+ pRes = Aig_CreateAnd( pMan, Vec_PtrSize(vNames)/2 );
+ else if ( Symbol == '|' )
+ pRes = Aig_CreateOr( pMan, Vec_PtrSize(vNames)/2 );
+ else if ( Symbol == '^' )
+ pRes = Aig_CreateExor( pMan, Vec_PtrSize(vNames)/2 );
+ return Aig_NotCond( pRes, fCompl );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////