summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abc.dsp8
-rw-r--r--src/aig/aig/aig.h3
-rw-r--r--src/aig/aig/aigMan.c19
-rw-r--r--src/aig/aig/aigUtil.c22
-rw-r--r--src/aig/fra/fraCore.c1
-rw-r--r--src/aig/fra/fraInd.c57
-rw-r--r--src/aig/ntl/ntl.h164
-rw-r--r--src/aig/nwk/nwk.h136
-rw-r--r--src/aig/saig/module.make4
-rw-r--r--src/aig/saig/saig.h5
-rw-r--r--src/aig/saig/saigIoa.c399
-rw-r--r--src/aig/saig/saigTrans.c422
-rw-r--r--src/base/abc/abc.h753
-rw-r--r--src/base/abci/abc.c302
-rw-r--r--src/base/abci/abcDar.c65
-rw-r--r--src/base/abci/abcMiter.c2
-rw-r--r--src/base/abci/abcVerify.c6
-rw-r--r--src/base/main/main.h86
-rw-r--r--src/base/main/mainInt.h34
-rw-r--r--src/misc/vec/vec.h4
20 files changed, 1922 insertions, 570 deletions
diff --git a/abc.dsp b/abc.dsp
index f856eec0..716ef21e 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3266,6 +3266,10 @@ SOURCE=.\src\aig\saig\saigInter.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\saig\saigIoa.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
@@ -3284,6 +3288,10 @@ SOURCE=.\src\aig\saig\saigRetStep.c
SOURCE=.\src\aig\saig\saigScl.c
# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigTrans.c
+# End Source File
# End Group
# Begin Group "bbr"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index bbb5cb6e..6987412d 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -135,6 +135,7 @@ struct Aig_Man_t_
Vec_Int_t * vLevelR; // the reverse level of the nodes
int nLevelMax; // maximum number of levels
void * pData; // the temporary data
+ void * pData2; // the temporary data
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
int fAddStrash; // performs additional strashing
@@ -497,6 +498,7 @@ extern int Aig_ManCleanup( Aig_Man_t * p );
extern int Aig_ManPiCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
+extern void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
/*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p );
extern void Aig_ManStopMemory( Aig_Man_t * p );
@@ -625,6 +627,7 @@ extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
extern void Aig_ManSetPioNumbers( Aig_Man_t * p );
extern void Aig_ManCleanPioNumbers( Aig_Man_t * p );
extern int Aig_ManCountChoices( Aig_Man_t * p );
+extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
extern unsigned Aig_ManRandom( int fReset );
/*=== aigWin.c =========================================================*/
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 47ee8d4d..669691f4 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -359,6 +359,25 @@ void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
printf( "\n" );
}
+/**Function*************************************************************
+
+ Synopsis [Sets the number of registers in the AIG manager.]
+
+ Description [This procedure should be called after the manager is
+ fully constructed.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs )
+{
+ p->nRegs = nRegs;
+ p->nTruePis = Aig_ManPiNum(p) - nRegs;
+ p->nTruePos = Aig_ManPoNum(p) - nRegs;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index a01e9582..7b64d562 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -992,6 +992,28 @@ void Aig_ManPrintControlFanouts( Aig_Man_t * p )
/**Function*************************************************************
+ Synopsis [Returns the composite name of the file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+ static char Buffer[1000];
+ char * pDot;
+ strcpy( Buffer, pBase );
+ if ( (pDot = strrchr( Buffer, '.' )) )
+ *pDot = 0;
+ strcat( Buffer, pSuffix );
+ return Buffer;
+}
+
+/**Function*************************************************************
+
Synopsis [Creates a sequence or random numbers.]
Description []
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 11e69b59..92a3f00b 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -411,6 +411,7 @@ p->timeTrav += clock() - clk2;
}
else
{
+ Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
Aig_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->pManFraig = NULL;
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 99b62856..3be0e3f6 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -616,6 +616,63 @@ finish:
return pManAigNew;
}
+/**Function*************************************************************
+
+ Synopsis [Outputs a set of pairs of equivalent nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
+{
+ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
+ FILE * pFile;
+ char * pFilePairs;
+ Aig_Man_t * pMan, * pNew;
+ Aig_Obj_t * pObj, * pRepr;
+ int * pNum2Id;
+ int i, Counter = 0;
+ pMan = Saig_ManReadBlif( pFileName );
+ if ( pMan == NULL )
+ return 0;
+ // perform seq SAT sweeping
+ pNew = Fra_FraigInduction( pMan, pParams );
+ if ( pNew == NULL )
+ {
+ Aig_ManStop( pMan );
+ return 0;
+ }
+ if ( pParams->fVerbose )
+ {
+ printf( "Original AIG: " );
+ Aig_ManPrintStats( pMan );
+ printf( "Reduced AIG: " );
+ Aig_ManPrintStats( pNew );
+ }
+ Aig_ManStop( pNew );
+ pNum2Id = pMan->pData;
+ // write the output file
+ pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
+ pFile = fopen( pFilePairs, "w" );
+ Aig_ManForEachObj( pMan, pObj, i )
+ if ( (pRepr = pMan->pReprs[pObj->Id]) )
+ {
+ fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
+ Counter++;
+ }
+ fclose( pFile );
+ if ( pParams->fVerbose )
+ {
+ printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
+ }
+ Aig_ManStop( pMan );
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index c4950650..4179754c 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: ntl.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
***********************************************************************/
@@ -145,8 +145,18 @@ struct Ntl_Lut_t_
////////////////////////////////////////////////////////////////////////
/// INLINED FUNCTIONS ///
////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
-static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p ) { return Vec_PtrEntry( p->vModels, 0 ); }
+static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p ) { return (Ntl_Mod_t *)Vec_PtrEntry( p->vModels, 0 ); }
static inline int Ntl_ModelPiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI]; }
static inline int Ntl_ModelPoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO]; }
@@ -157,8 +167,8 @@ static inline int Ntl_ModelBoxNum( Ntl_Mod_t * p ) { return p->nO
static inline int Ntl_ModelCiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; }
static inline int Ntl_ModelCoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; }
-static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i ) { return Vec_PtrEntry(p->vPis, i); }
-static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return Vec_PtrEntry(p->vPos, i); }
+static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i ) { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i); }
+static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i ) { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline char * Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; }
static inline char * Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; }
@@ -188,7 +198,7 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
////////////////////////////////////////////////////////////////////////
#define Ntl_ManForEachModel( p, pMod, i ) \
- Vec_PtrForEachEntry( p->vModels, pMod, i )
+ for ( i = 0; (i < Vec_PtrSize(p->vModels)) && (((pMod) = (Ntl_Mod_t*)Vec_PtrEntry(p->vModels, i)), 1); i++ )
#define Ntl_ManForEachCiNet( p, pNet, i ) \
Vec_PtrForEachEntry( p->vCis, pNet, i )
#define Ntl_ManForEachCoNet( p, pNet, i ) \
@@ -201,20 +211,20 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
#define Ntl_ModelForEachPi( pNwk, pObj, i ) \
- Vec_PtrForEachEntry( pNwk->vPis, pObj, i )
+ for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ )
#define Ntl_ModelForEachPo( pNwk, pObj, i ) \
- Vec_PtrForEachEntry( pNwk->vPos, pObj, i )
+ for ( i = 0; (i < Vec_PtrSize(pNwk->vPos)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPos, i)), 1); i++ )
#define Ntl_ModelForEachObj( pNwk, pObj, i ) \
- for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
if ( pObj == NULL ) {} else
#define Ntl_ModelForEachLatch( pNwk, pObj, i ) \
- for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
- if ( (pObj) == NULL || !Ntl_ObjIsLatch(pObj) ) {} else
+ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+ if ( (pObj) == NULL || !Ntl_ObjIsLatch((Ntl_Obj_t*)pObj) ) {} else
#define Ntl_ModelForEachNode( pNwk, pObj, i ) \
- for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else
#define Ntl_ModelForEachBox( pNwk, pObj, i ) \
- for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+ for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
#define Ntl_ModelForEachNet( pNwk, pNet, i ) \
for ( i = 0; i < pNwk->nTableSize; i++ ) \
@@ -230,84 +240,84 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
////////////////////////////////////////////////////////////////////////
/*=== ntlCore.c ==========================================================*/
-extern int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
-extern int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern ABC_DLL int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern ABC_DLL int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
/*=== ntlEc.c ==========================================================*/
-extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
-extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
+extern ABC_DLL void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
+extern ABC_DLL Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
/*=== ntlExtract.c ==========================================================*/
-extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
-extern Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p );
-extern Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
+extern ABC_DLL Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
+extern ABC_DLL Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
+extern ABC_DLL Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p );
+extern ABC_DLL Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
/*=== ntlInsert.c ==========================================================*/
-extern Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
-extern Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
-extern Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
+extern ABC_DLL Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern ABC_DLL Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern ABC_DLL Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
/*=== ntlCheck.c ==========================================================*/
-extern int Ntl_ManCheck( Ntl_Man_t * pMan );
-extern int Ntl_ModelCheck( Ntl_Mod_t * pModel );
-extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
+extern ABC_DLL int Ntl_ManCheck( Ntl_Man_t * pMan );
+extern ABC_DLL int Ntl_ModelCheck( Ntl_Mod_t * pModel );
+extern ABC_DLL void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
/*=== ntlMan.c ============================================================*/
-extern Ntl_Man_t * Ntl_ManAlloc();
-extern void Ntl_ManCleanup( Ntl_Man_t * p );
-extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p );
-extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p );
-extern void Ntl_ManFree( Ntl_Man_t * p );
-extern int Ntl_ManIsComb( Ntl_Man_t * p );
-extern int Ntl_ManLatchNum( Ntl_Man_t * p );
-extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
-extern void Ntl_ManPrintStats( Ntl_Man_t * p );
-extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
-extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
-extern Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
-extern Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
-extern void Ntl_ModelFree( Ntl_Mod_t * p );
+extern ABC_DLL Ntl_Man_t * Ntl_ManAlloc();
+extern ABC_DLL void Ntl_ManCleanup( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p );
+extern ABC_DLL void Ntl_ManFree( Ntl_Man_t * p );
+extern ABC_DLL int Ntl_ManIsComb( Ntl_Man_t * p );
+extern ABC_DLL int Ntl_ManLatchNum( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
+extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p );
+extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
+extern ABC_DLL Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
+extern ABC_DLL Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
+extern ABC_DLL Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
+extern ABC_DLL void Ntl_ModelFree( Ntl_Mod_t * p );
/*=== ntlMap.c ============================================================*/
-extern Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars );
-extern Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p );
-extern Vec_Ptr_t * Ntl_MappingFpga( Aig_Man_t * p );
-extern Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p );
+extern ABC_DLL Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars );
+extern ABC_DLL Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p );
+extern ABC_DLL Vec_Ptr_t * Ntl_MappingFpga( Aig_Man_t * p );
+extern ABC_DLL Vec_Ptr_t * Ntl_MappingIf( Ntl_Man_t * pMan, Aig_Man_t * p );
/*=== ntlObj.c ============================================================*/
-extern Ntl_Obj_t * Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
-extern Ntl_Obj_t * Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
-extern Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
-extern Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
-extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
-extern Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
-extern Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
-extern char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
-extern char * Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
-extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
+extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
+extern ABC_DLL char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
+extern ABC_DLL char * Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
+extern ABC_DLL char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
/*=== ntlSweep.c ==========================================================*/
-extern int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
+extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
/*=== ntlTable.c ==========================================================*/
-extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
-extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
-extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
-extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
-extern int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
-extern void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
-extern int Ntl_ModelCountNets( Ntl_Mod_t * p );
+extern ABC_DLL Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
+extern ABC_DLL Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
+extern ABC_DLL int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
+extern ABC_DLL int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern ABC_DLL int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+extern ABC_DLL void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
+extern ABC_DLL int Ntl_ModelCountNets( Ntl_Mod_t * p );
/*=== ntlTime.c ==========================================================*/
-extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p );
+extern ABC_DLL Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p );
/*=== ntlReadBlif.c ==========================================================*/
-extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
+extern ABC_DLL Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
-extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
-extern void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
/*=== ntlUtil.c ==========================================================*/
-extern int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
-extern int Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
-extern Ntl_Net_t * Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
-extern int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
-extern Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p );
-extern Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p );
-extern void Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
-extern void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
-extern int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
-extern void Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
-extern void Ntl_ManTransformInitValues( Ntl_Man_t * p );
+extern ABC_DLL int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
+extern ABC_DLL int Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
+extern ABC_DLL Ntl_Net_t * Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
+extern ABC_DLL int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
+extern ABC_DLL Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p );
+extern ABC_DLL Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p );
+extern ABC_DLL void Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
+extern ABC_DLL void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
+extern ABC_DLL int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
+extern ABC_DLL void Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
+extern ABC_DLL void Ntl_ManTransformInitValues( Ntl_Man_t * p );
#ifdef __cplusplus
}
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index b0edd243..6c78ca87 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: nwk.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: nwk.h,v 1.1 2008/05/14 22:13:09 wudenni Exp $]
***********************************************************************/
@@ -29,6 +29,8 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
+#pragma warning( disable : 4273 )
+
#include "aig.h"
#include "hop.h"
#include "tim.h"
@@ -117,6 +119,16 @@ struct Nwk_Obj_t_
////////////////////////////////////////////////////////////////////////
/// INLINED FUNCTIONS ///
////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
static inline int Nwk_ManCiNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_CI]; }
static inline int Nwk_ManCoNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_CO]; }
@@ -124,9 +136,9 @@ static inline int Nwk_ManNodeNum( Nwk_Man_t * p ) { return p->nO
static inline int Nwk_ManLatchNum( Nwk_Man_t * p ) { return p->nObjs[NWK_OBJ_LATCH]; }
static inline int Nwk_ManObjNumMax( Nwk_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
-static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCis, i ); }
-static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCos, i ); }
-static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i ) { return Vec_PtrEntry( p->vObjs, i ); }
+static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i ) { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCis, i ); }
+static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i ) { return (Nwk_Obj_t *)Vec_PtrEntry( p->vCos, i ); }
+static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i ) { return (Nwk_Obj_t *)Vec_PtrEntry( p->vObjs, i ); }
static inline int Nwk_ObjId( Nwk_Obj_t * p ) { return p->Id; }
static inline int Nwk_ObjPioNum( Nwk_Obj_t * p ) { return p->PioId; }
@@ -216,76 +228,76 @@ static inline int Nwk_ManTimeMore( float f1, float f2, float Eps ) { r
////////////////////////////////////////////////////////////////////////
/*=== nwkAig.c ==========================================================*/
-extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose );
/*=== nwkBidec.c ==========================================================*/
-extern void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
-extern Hop_Obj_t * Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
+extern ABC_DLL void Nwk_ManBidecResyn( Nwk_Man_t * pNtk, int fVerbose );
+extern ABC_DLL Hop_Obj_t * Nwk_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
/*=== nwkCheck.c ==========================================================*/
-extern int Nwk_ManCheck( Nwk_Man_t * p );
+extern ABC_DLL int Nwk_ManCheck( Nwk_Man_t * p );
/*=== nwkDfs.c ==========================================================*/
-extern int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
-extern int Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
-extern int Nwk_ManLevel( Nwk_Man_t * pNtk );
-extern int Nwk_ManLevelMax( Nwk_Man_t * pNtk );
-extern Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk );
-extern Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk );
-extern Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk );
-extern Vec_Ptr_t * Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
-extern void Nwk_ManSupportSum( Nwk_Man_t * pNtk );
-extern int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
+extern ABC_DLL int Nwk_ManVerifyTopoOrder( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManLevelBackup( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManLevel( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManLevelMax( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Vec_t * Nwk_ManLevelize( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManDfs( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManDfsNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManDfsReverse( Nwk_Man_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManSupportNodes( Nwk_Man_t * pNtk, Nwk_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL void Nwk_ManSupportSum( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ObjMffcLabel( Nwk_Obj_t * pNode );
/*=== nwkFanio.c ==========================================================*/
-extern void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
-extern int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
-extern void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
-extern void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
-extern void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
-extern void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
-extern void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
+extern ABC_DLL void Nwk_ObjCollectFanins( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL void Nwk_ObjCollectFanouts( Nwk_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL int Nwk_ObjFindFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern ABC_DLL int Nwk_ObjFindFanout( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanout );
+extern ABC_DLL void Nwk_ObjAddFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern ABC_DLL void Nwk_ObjDeleteFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFanin );
+extern ABC_DLL void Nwk_ObjPatchFanin( Nwk_Obj_t * pObj, Nwk_Obj_t * pFaninOld, Nwk_Obj_t * pFaninNew );
+extern ABC_DLL void Nwk_ObjTransferFanout( Nwk_Obj_t * pNodeFrom, Nwk_Obj_t * pNodeTo );
+extern ABC_DLL void Nwk_ObjReplace( Nwk_Obj_t * pNodeOld, Nwk_Obj_t * pNodeNew );
/*=== nwkFlow.c ============================================================*/
-extern Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
-extern Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
+extern ABC_DLL Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose );
/*=== nwkMan.c ============================================================*/
-extern Nwk_Man_t * Nwk_ManAlloc();
-extern void Nwk_ManFree( Nwk_Man_t * p );
-extern void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
+extern ABC_DLL Nwk_Man_t * Nwk_ManAlloc();
+extern ABC_DLL void Nwk_ManFree( Nwk_Man_t * p );
+extern ABC_DLL void Nwk_ManPrintStats( Nwk_Man_t * p, If_Lib_t * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
/*=== nwkMap.c ============================================================*/
-extern Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
+extern ABC_DLL Nwk_Man_t * Nwk_MappingIf( Aig_Man_t * p, Tim_Man_t * pManTime, If_Par_t * pPars );
/*=== nwkObj.c ============================================================*/
-extern Nwk_Obj_t * Nwk_ManCreateCi( Nwk_Man_t * pMan, int nFanouts );
-extern Nwk_Obj_t * Nwk_ManCreateCo( Nwk_Man_t * pMan );
-extern Nwk_Obj_t * Nwk_ManCreateNode( Nwk_Man_t * pMan, int nFanins, int nFanouts );
-extern Nwk_Obj_t * Nwk_ManCreateBox( Nwk_Man_t * pMan, int nFanins, int nFanouts );
-extern Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * pMan );
-extern void Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
-extern void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
+extern ABC_DLL Nwk_Obj_t * Nwk_ManCreateCi( Nwk_Man_t * pMan, int nFanouts );
+extern ABC_DLL Nwk_Obj_t * Nwk_ManCreateCo( Nwk_Man_t * pMan );
+extern ABC_DLL Nwk_Obj_t * Nwk_ManCreateNode( Nwk_Man_t * pMan, int nFanins, int nFanouts );
+extern ABC_DLL Nwk_Obj_t * Nwk_ManCreateBox( Nwk_Man_t * pMan, int nFanins, int nFanouts );
+extern ABC_DLL Nwk_Obj_t * Nwk_ManCreateLatch( Nwk_Man_t * pMan );
+extern ABC_DLL void Nwk_ManDeleteNode( Nwk_Obj_t * pObj );
+extern ABC_DLL void Nwk_ManDeleteNode_rec( Nwk_Obj_t * pObj );
/*=== nwkSpeedup.c ============================================================*/
-extern Aig_Man_t * Nwk_ManSpeedup( Nwk_Man_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
+extern ABC_DLL Aig_Man_t * Nwk_ManSpeedup( Nwk_Man_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
/*=== nwkStrash.c ============================================================*/
-extern Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk );
+extern ABC_DLL Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk );
/*=== nwkTiming.c ============================================================*/
-extern int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk );
-extern void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinDelays );
-extern float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
-extern void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
-extern void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManVerifyTiming( Nwk_Man_t * pNtk );
+extern ABC_DLL void Nwk_ManDelayTraceSortPins( Nwk_Obj_t * pNode, int * pPinPerm, float * pPinDelays );
+extern ABC_DLL float Nwk_ManDelayTraceLut( Nwk_Man_t * pNtk );
+extern ABC_DLL void Nwk_ManDelayTracePrint( Nwk_Man_t * pNtk );
+extern ABC_DLL void Nwk_ManUpdate( Nwk_Obj_t * pObj, Nwk_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL int Nwk_ManVerifyLevel( Nwk_Man_t * pNtk );
/*=== nwkUtil.c ============================================================*/
-extern void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
-extern int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
-extern int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk );
-extern int Nwk_ManPiNum( Nwk_Man_t * pNtk );
-extern int Nwk_ManPoNum( Nwk_Man_t * pNtk );
-extern int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
-extern int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
-extern int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
-extern void Nwk_ObjPrint( Nwk_Obj_t * pObj );
-extern void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
-extern void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
-extern void Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
-extern void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
+extern ABC_DLL void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManGetFaninMax( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManPiNum( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManPoNum( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_ManGetAigNodeNum( Nwk_Man_t * pNtk );
+extern ABC_DLL int Nwk_NodeCompareLevelsIncrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern ABC_DLL int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 );
+extern ABC_DLL void Nwk_ObjPrint( Nwk_Obj_t * pObj );
+extern ABC_DLL void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
+extern ABC_DLL void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
+extern ABC_DLL void Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
+extern ABC_DLL void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
#ifdef __cplusplus
}
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 68c49133..ea122bbf 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,8 +1,10 @@
SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigInter.c \
+ src/aig/saig/saigIoa.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
src/aig/saig/saigRetStep.c \
- src/aig/saig/saigScl.c
+ src/aig/saig/saigScl.c \
+ src/aig/saig/saigTrans.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b9b7de40..c8efab40 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -79,6 +79,9 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
+/*=== saigIoa.c ==========================================================*/
+extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
+extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
/*=== saigInter.c ==========================================================*/
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
/*=== saigPhase.c ==========================================================*/
@@ -92,6 +95,8 @@ extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, in
extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+/*=== saigTrans.c ==========================================================*/
+extern Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose );
#ifdef __cplusplus
}
diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c
new file mode 100644
index 00000000..70870fe9
--- /dev/null
+++ b/src/aig/saig/saigIoa.c
@@ -0,0 +1,399 @@
+/**CFile****************************************************************
+
+ FileName [saigIoa.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Input/output for sequential AIGs using BLIF files.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigIoa.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ static char Buffer[16];
+ if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
+ sprintf( Buffer, "n%0*d", Aig_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
+ else if ( Saig_ObjIsPi(p, pObj) )
+ sprintf( Buffer, "pi%0*d", Aig_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) );
+ else if ( Saig_ObjIsPo(p, pObj) )
+ sprintf( Buffer, "po%0*d", Aig_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) );
+ else if ( Saig_ObjIsLo(p, pObj) )
+ sprintf( Buffer, "lo%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) );
+ else if ( Saig_ObjIsLi(p, pObj) )
+ sprintf( Buffer, "li%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) );
+ else
+ assert( 0 );
+ return Buffer;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
+{
+ FILE * pFile;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i;
+ if ( Aig_ManPoNum(p) == 0 )
+ {
+ printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
+ return;
+ }
+ Aig_ManSetPioNumbers( p );
+ // write input file
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
+ return;
+ }
+ fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
+ fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
+ fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n",
+ Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p),
+ Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
+ fprintf( pFile, ".model %s\n", p->pName );
+ // write primary inputs
+ fprintf( pFile, ".inputs" );
+ Aig_ManForEachPiSeq( p, pObj, i )
+ fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+ fprintf( pFile, "\n" );
+ // write primary outputs
+ fprintf( pFile, ".outputs" );
+ Aig_ManForEachPoSeq( p, pObj, i )
+ fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+ fprintf( pFile, "\n" );
+ // write registers
+ if ( Aig_ManRegNum(p) )
+ {
+ Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
+ {
+ fprintf( pFile, ".latch" );
+ fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
+ fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
+ fprintf( pFile, " 0\n" );
+ }
+ }
+ // check if constant is used
+ if ( Aig_ObjRefs(Aig_ManConst1(p)) )
+ fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
+ // write the nodes in the DFS order
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ fprintf( pFile, ".names" );
+ fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
+ fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
+ fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+ fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
+ }
+ // write the POs
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ fprintf( pFile, ".names" );
+ fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
+ fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
+ fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
+ }
+ fprintf( pFile, ".end\n" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads one token from file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Saig_ManReadToken( FILE * pFile )
+{
+ static char Buffer[1000];
+ if ( fscanf( pFile, "%s", Buffer ) == 1 )
+ return Buffer;
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the corresponding number.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Saig_ManReadNumber( Aig_Man_t * p, char * pToken )
+{
+ if ( pToken[0] == 'n' )
+ return atoi( pToken + 1 );
+ if ( pToken[0] == 'p' )
+ return atoi( pToken + 2 );
+ if ( pToken[0] == 'l' )
+ return atoi( pToken + 2 );
+ assert( 0 );
+ return -1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the corresponding node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken )
+{
+ int Num;
+ if ( pToken[0] == 'n' )
+ {
+ Num = atoi( pToken + 1 );
+ return Aig_ManObj( p, pNum2Id[Num] );
+ }
+ if ( pToken[0] == 'p' )
+ {
+ pToken++;
+ if ( pToken[0] == 'i' )
+ {
+ Num = atoi( pToken + 1 );
+ return Aig_ManPi( p, Num );
+ }
+ if ( pToken[0] == 'o' )
+ return NULL;
+ assert( 0 );
+ return NULL;
+ }
+ if ( pToken[0] == 'l' )
+ {
+ pToken++;
+ if ( pToken[0] == 'o' )
+ {
+ Num = atoi( pToken + 1 );
+ return Saig_ManLo( p, Num );
+ }
+ if ( pToken[0] == 'i' )
+ return NULL;
+ assert( 0 );
+ return NULL;
+ }
+ assert( 0 );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads BLIF previously dumped by Saig_ManDumpBlif().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManReadBlif( char * pFileName )
+{
+ FILE * pFile;
+ Aig_Man_t * p;
+ Aig_Obj_t * pFanin0, * pFanin1, * pNode;
+ char * pToken;
+ int i, nPis, nPos, nRegs, Number;
+ int * pNum2Id = NULL; // mapping of node numbers in the file into AIG node IDs
+ // open the file
+ pFile = fopen( pFileName, "r" );
+ if ( pFile == NULL )
+ {
+ printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
+ return NULL;
+ }
+ // skip through the comments
+ for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
+ // get he model
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
+ // start the package
+ p = Aig_ManStart( 10000 );
+ p->pName = Aig_UtilStrsav( pToken );
+ p->pSpec = Aig_UtilStrsav( pFileName );
+ // count PIs
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL || strcmp( pToken, ".inputs" ) )
+ { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
+ for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
+ // count POs
+ if ( pToken == NULL || strcmp( pToken, ".outputs" ) )
+ { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
+ for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
+ // count latches
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
+ for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
+ {
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
+ }
+ // create PIs and LOs
+ for ( i = 0; i < nPis + nRegs; i++ )
+ Aig_ObjCreatePi( p );
+ Aig_ManSetRegNum( p, nRegs );
+ // create nodes
+ for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
+ {
+ // first token
+ pToken = Saig_ManReadToken( pFile );
+ if ( i == 0 && pToken[0] == 'n' )
+ { // constant node
+ // read 1
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL || strcmp( pToken, "1" ) )
+ { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
+ // read next
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
+ continue;
+ }
+ pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );
+
+ // second token
+ pToken = Saig_ManReadToken( pFile );
+ if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
+ { // buffer
+ // read complemented attribute
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
+ if ( pToken[0] == '0' )
+ pFanin0 = Aig_Not(pFanin0);
+ // read 1
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL || strcmp( pToken, "1" ) )
+ { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
+ Aig_ObjCreatePo( p, pFanin0 );
+ // read next
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
+ continue;
+ }
+
+ // third token
+ // regular node
+ pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
+ pToken = Saig_ManReadToken( pFile );
+ Number = Saig_ManReadNumber( p, pToken );
+ // allocate mapping
+ if ( pNum2Id == NULL )
+ {
+ extern double pow( double x, double y );
+ int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
+ pNum2Id = CALLOC( int, Size );
+ }
+
+ // other tokens
+ // get the complemented attributes
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
+ if ( pToken[0] == '0' )
+ pFanin0 = Aig_Not(pFanin0);
+ if ( pToken[1] == '0' )
+ pFanin1 = Aig_Not(pFanin1);
+ // read 1
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL || strcmp( pToken, "1" ) )
+ { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
+ // read next
+ pToken = Saig_ManReadToken( pFile );
+ if ( pToken == NULL )
+ { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }
+
+ // create new node
+ pNode = Aig_And( p, pFanin0, pFanin1 );
+ if ( Aig_IsComplement(pNode) )
+ { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
+ // set mapping
+ pNum2Id[ Number ] = pNode->Id;
+ }
+ if ( pToken == NULL || strcmp( pToken, ".end" ) )
+ { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
+ if ( nPos + nRegs != Aig_ManPoNum(p) )
+ { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
+ // add non-node objects to the mapping
+ Aig_ManForEachPi( p, pNode, i )
+ pNum2Id[pNode->Id] = pNode->Id;
+// FREE( pNum2Id );
+ p->pData = pNum2Id;
+ // check the new manager
+ Aig_ManSetRegNum( p, nRegs );
+ if ( !Aig_ManCheck(p) )
+ printf( "Saig_ManReadBlif(): Check has failed.\n" );
+ return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c
new file mode 100644
index 00000000..b0039276
--- /dev/null
+++ b/src/aig/saig/saigTrans.c
@@ -0,0 +1,422 @@
+/**CFile****************************************************************
+
+ FileName [saigTrans.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Dynamic simplication of the transition relation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigTrans.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+/*
+ A similar approach is presented in the his paper:
+ A. Kuehlmann. Dynamic transition relation simplification for
+ bounded property checking. ICCAD'04, pp. 50-57.
+*/
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Maps a node/frame into a node of a different manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Saig_ManStartMap1( Aig_Man_t * p, int nFrames )
+{
+ Vec_Int_t * vMap;
+ int i;
+ assert( p->pData == NULL );
+ vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames );
+ for ( i = 0; i < vMap->nCap; i++ )
+ vMap->pArray[i] = -1;
+ vMap->nSize = vMap->nCap;
+ p->pData = vMap;
+}
+static inline void Saig_ManStopMap1( Aig_Man_t * p )
+{
+ assert( p->pData != NULL );
+ Vec_IntFree( p->pData );
+ p->pData = NULL;
+}
+static inline int Saig_ManHasMap1( Aig_Man_t * p )
+{
+ return (int)(p->pData != NULL);
+}
+static inline void Saig_ManSetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew )
+{
+ Vec_Int_t * vMap = p->pData;
+ int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+ assert( !Aig_IsComplement(pOld) );
+ assert( !Aig_IsComplement(pNew) );
+ Vec_IntWriteEntry( vMap, nOffset, pNew->Id );
+}
+static inline int Saig_ManGetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1 )
+{
+ Vec_Int_t * vMap = p->pData;
+ int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+ return Vec_IntEntry( vMap, nOffset );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Maps a node/frame into a node/frame of a different manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Saig_ManStartMap2( Aig_Man_t * p, int nFrames )
+{
+ Vec_Int_t * vMap;
+ int i;
+ assert( p->pData2 == NULL );
+ vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames * 2 );
+ for ( i = 0; i < vMap->nCap; i++ )
+ vMap->pArray[i] = -1;
+ vMap->nSize = vMap->nCap;
+ p->pData2 = vMap;
+}
+static inline void Saig_ManStopMap2( Aig_Man_t * p )
+{
+ assert( p->pData2 != NULL );
+ Vec_IntFree( p->pData2 );
+ p->pData2 = NULL;
+}
+static inline int Saig_ManHasMap2( Aig_Man_t * p )
+{
+ return (int)(p->pData2 != NULL);
+}
+static inline void Saig_ManSetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew, int f2 )
+{
+ Vec_Int_t * vMap = p->pData2;
+ int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+ assert( !Aig_IsComplement(pOld) );
+ assert( !Aig_IsComplement(pNew) );
+ Vec_IntWriteEntry( vMap, 2*nOffset + 0, pNew->Id );
+ Vec_IntWriteEntry( vMap, 2*nOffset + 1, f2 );
+}
+static inline int Saig_ManGetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, int * pf2 )
+{
+ Vec_Int_t * vMap = p->pData2;
+ int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
+ *pf2 = Vec_IntEntry( vMap, 2*nOffset + 1 );
+ return Vec_IntEntry( vMap, 2*nOffset );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Create mapping for the first nFrames timeframes of pAig.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManCreateMapping( Aig_Man_t * pAig, Aig_Man_t * pFrames, int nFrames )
+{
+ Aig_Obj_t * pObj, * pObjFrame, * pObjRepr;
+ int i, f, iNum, iFrame;
+ assert( pFrames->pReprs != NULL ); // mapping from nodes into their representatives
+ // start step mapping for both orignal manager and fraig
+ Saig_ManStartMap2( pAig, nFrames );
+ Saig_ManStartMap2( pFrames, 1 );
+ // for each object in each frame
+ for ( f = 0; f < nFrames; f++ )
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ // get the frame object
+ iNum = Saig_ManGetMap1( pAig, pObj, f );
+ pObjFrame = Aig_ManObj( pFrames, iNum );
+ // if the node has no prototype, map it into itself
+ if ( pObjFrame == NULL )
+ {
+ Saig_ManSetMap2( pAig, pObj, f, pObj, f );
+ continue;
+ }
+ // get the representative object
+ pObjRepr = Aig_ObjRepr( pFrames, pObjFrame );
+ if ( pObjRepr == NULL )
+ pObjRepr = pObjFrame;
+ // check if this is the first time this object is reached
+ if ( Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame ) == -1 )
+ Saig_ManSetMap2( pFrames, pObjRepr, 0, pObj, f );
+ // set the map for the main object
+ iNum = Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame );
+ Saig_ManSetMap2( pAig, pObj, f, Aig_ManObj(pAig, iNum), iFrame );
+ }
+ Saig_ManStopMap2( pFrames );
+ assert( Saig_ManHasMap2(pAig) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Unroll without initialization.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesNonInitial( Aig_Man_t * pAig, int nFrames )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, f;
+ assert( Saig_ManRegNum(pAig) > 0 );
+ // start node map
+ Saig_ManStartMap1( pAig, nFrames );
+ // start the new manager
+ pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+ // create variables for register outputs
+ Saig_ManForEachLo( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ // add timeframes
+ for ( f = 0; f < nFrames; f++ )
+ {
+ // create PI nodes for this frame
+ Saig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create POs for this frame
+ Saig_ManForEachPo( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ // save register inputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ // save the mapping
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ assert( pObj->pData != NULL );
+ Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+ }
+ // quit if the last frame
+ if ( f == nFrames - 1 )
+ break;
+ // transfer to register outputs
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ pObjLo->pData = pObjLi->pData;
+ }
+ // remember register outputs
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ Aig_ObjCreatePo( pFrames, pObjLi->pData );
+ Aig_ManCleanup( pFrames );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Unroll with initialization and mapping.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesInitialMapped( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pRepr;
+ int i, f, iNum1, iNum2, iFrame2;
+ assert( nFrames <= nFramesMax );
+ assert( Saig_ManRegNum(pAig) > 0 );
+ // start node map
+ Saig_ManStartMap1( pAig, nFramesMax );
+ // start the new manager
+ pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFramesMax );
+ // create variables for register outputs
+ if ( fInit )
+ {
+ Saig_ManForEachLo( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ManConst0( pFrames );
+ Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(pObj->pData) );
+ }
+ }
+ else
+ {
+ // create PIs first
+ for ( f = 0; f < nFramesMax; f++ )
+ Saig_ManForEachPi( pAig, pObj, i )
+ Aig_ObjCreatePi( pFrames );
+ // create registers second
+ Saig_ManForEachLo( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular(pObj->pData) );
+ }
+ }
+ // add timeframes
+ for ( f = 0; f < nFramesMax; f++ )
+ {
+ // map the constant node
+ pObj = Aig_ManConst1(pAig);
+ pObj->pData = Aig_ManConst1( pFrames );
+ Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+ // create PI nodes for this frame
+ Saig_ManForEachPi( pAig, pObj, i )
+ {
+ if ( fInit )
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ else
+ pObj->pData = Aig_ManPi( pFrames, f * Saig_ManPiNum(pAig) + i );
+ Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+ }
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ {
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+ if ( !Saig_ManHasMap2(pAig) )
+ continue;
+ if ( f < nFrames )
+ {
+ // get the mapping for this node
+ iNum2 = Saig_ManGetMap2( pAig, pObj, f, &iFrame2 );
+ }
+ else
+ {
+ // get the mapping for this node
+ iNum2 = Saig_ManGetMap2( pAig, pObj, nFrames-1, &iFrame2 );
+ iFrame2 += f - (nFrames-1);
+ }
+ assert( iNum2 != -1 );
+ assert( f >= iFrame2 );
+ // get the corresponding frames node
+ iNum1 = Saig_ManGetMap1( pAig, Aig_ManObj(pAig, iNum2), iFrame2 );
+ pRepr = Aig_ManObj( pFrames, iNum1 );
+ // compare the phases of these nodes
+ pObj->pData = Aig_NotCond( pRepr, pRepr->fPhase ^ Aig_ObjPhaseReal(pObj->pData) );
+ }
+ // create POs for this frame
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+ Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+ }
+ // save register inputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ {
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ Saig_ManSetMap1( pAig, pObj, f, Aig_Regular(pObj->pData) );
+ }
+ // quit if the last frame
+ if ( f == nFramesMax - 1 )
+ break;
+ // transfer to register outputs
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ {
+ pObjLo->pData = pObjLi->pData;
+ if ( !fInit )
+ Saig_ManSetMap1( pAig, pObjLo, f+1, Aig_Regular(pObjLo->pData) );
+ }
+ }
+ if ( !fInit )
+ {
+ // create registers
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ Aig_ObjCreatePo( pFrames, pObjLi->pData );
+ // set register number
+ Aig_ManSetRegNum( pFrames, pAig->nRegs );
+ }
+ Aig_ManCleanup( pFrames );
+ Saig_ManStopMap1( pAig );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements dynamic simplification.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose )
+{
+ extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
+ Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
+ int clk, clkTotal = clock();
+ // create uninitialized timeframes with map1
+ pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
+ // perform fraiging for the unrolled timeframes
+clk = clock();
+ pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
+ // report the results
+ if ( fVerbose )
+ {
+ Aig_ManPrintStats( pFrames );
+ Aig_ManPrintStats( pFraig );
+PRT( "Fraiging", clock() - clk );
+ }
+ Aig_ManStop( pFraig );
+ assert( pFrames->pReprs != NULL );
+ // create AIG with map2
+ Saig_ManCreateMapping( pAig, pFrames, nFrames );
+ Aig_ManStop( pFrames );
+ Saig_ManStopMap1( pAig );
+ // create reduced initialized timeframes
+clk = clock();
+ pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
+PRT( "Mapped", clock() - clk );
+ // free mapping
+ Saig_ManStopMap2( pAig );
+clk = clock();
+ pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
+PRT( "Normal", clock() - clk );
+ // report the results
+ if ( fVerbose )
+ {
+ Aig_ManPrintStats( pRes1 );
+ Aig_ManPrintStats( pRes2 );
+ }
+ Aig_ManStop( pRes1 );
+ assert( !Saig_ManHasMap1(pAig) );
+ assert( !Saig_ManHasMap2(pAig) );
+ return pRes2;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 15043266..0cafa314 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: abc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: abc.h,v 1.1 2008/05/14 22:13:11 wudenni Exp $]
***********************************************************************/
@@ -29,6 +29,8 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
+#pragma warning( disable : 4273 )
+
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
@@ -224,6 +226,17 @@ struct Abc_Lib_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
+
// maximum/minimum operators
#define ABC_MIN(a,b) (((a) < (b))? (a) : (b))
#define ABC_MAX(a,b) (((a) > (b))? (a) : (b))
@@ -307,7 +320,7 @@ static inline bool Abc_NtkIsComb( Abc_Ntk_t * pNtk ) { return Ab
static inline bool Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); }
// creating simple objects
-extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PI ); }
static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO ); }
static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI ); }
@@ -508,410 +521,410 @@ static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
////////////////////////////////////////////////////////////////////////
/*=== abcAig.c ==========================================================*/
-extern Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtk );
-extern void Abc_AigFree( Abc_Aig_t * pMan );
-extern int Abc_AigCleanup( Abc_Aig_t * pMan );
-extern bool Abc_AigCheck( Abc_Aig_t * pMan );
-extern int Abc_AigLevel( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_AigConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t * Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType );
-extern Abc_Obj_t * Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType );
-extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
-extern Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
-extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
-extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
-extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
-extern void Abc_AigRehash( Abc_Aig_t * pMan );
-extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
-extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
-extern void Abc_AigPrintNode( Abc_Obj_t * pNode );
-extern bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
-extern void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
-extern void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets );
-extern void Abc_AigUpdateStop( Abc_Aig_t * pMan );
-extern void Abc_AigUpdateReset( Abc_Aig_t * pMan );
+extern ABC_DLL Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_AigFree( Abc_Aig_t * pMan );
+extern ABC_DLL int Abc_AigCleanup( Abc_Aig_t * pMan );
+extern ABC_DLL bool Abc_AigCheck( Abc_Aig_t * pMan );
+extern ABC_DLL int Abc_AigLevel( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t * Abc_AigConst1( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t * Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType );
+extern ABC_DLL Abc_Obj_t * Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType );
+extern ABC_DLL Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
+extern ABC_DLL Abc_Obj_t * Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
+extern ABC_DLL Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
+extern ABC_DLL void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
+extern ABC_DLL void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
+extern ABC_DLL void Abc_AigRehash( Abc_Aig_t * pMan );
+extern ABC_DLL bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
+extern ABC_DLL void Abc_AigPrintNode( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
+extern ABC_DLL void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
+extern ABC_DLL void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_AigUpdateStart( Abc_Aig_t * pMan, Vec_Ptr_t ** pvUpdatedNets );
+extern ABC_DLL void Abc_AigUpdateStop( Abc_Aig_t * pMan );
+extern ABC_DLL void Abc_AigUpdateReset( Abc_Aig_t * pMan );
/*=== abcAttach.c ==========================================================*/
-extern int Abc_NtkAttach( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkAttach( Abc_Ntk_t * pNtk );
/*=== abcBlifMv.c ==========================================================*/
-extern void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
-extern void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk );
-extern void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues );
-extern Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic );
-extern int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk );
-extern char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
-extern int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
+extern ABC_DLL void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkStrashBlifMv( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic );
+extern ABC_DLL int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk );
+extern ABC_DLL char * Abc_NodeConvertSopToMvSop( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
+extern ABC_DLL int Abc_NodeEvalMvCost( int nVars, Vec_Int_t * vSop0, Vec_Int_t * vSop1 );
/*=== abcBalance.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel );
/*=== abcCheck.c ==========================================================*/
-extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk );
-extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
-extern bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
-extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
-extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
-extern int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
-extern int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
-extern int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
-extern int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool Abc_NtkCheck( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
+extern ABC_DLL bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
+extern ABC_DLL int Abc_NtkIsAcyclicHierarchy( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkCheckUniqueCiNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
/*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
/*=== abcCut.c ==========================================================*/
-extern void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
-extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
-extern void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
-extern void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
-extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
+extern ABC_DLL void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern ABC_DLL void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
+extern ABC_DLL void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst );
+extern ABC_DLL void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj );
+extern ABC_DLL void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
/*=== abcDelay.c ==========================================================*/
-extern float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
+extern ABC_DLL float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib );
/*=== abcDfs.c ==========================================================*/
-extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
-extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t * Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
-extern Vec_Ptr_t * Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll );
-extern bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
-extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
-extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
-extern Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk );
-extern int Abc_NtkLevel( Abc_Ntk_t * pNtk );
-extern int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
-extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverseNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsReverseNodesContained( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsIter( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkDfsHie( Abc_Ntk_t * pNtk, int fCollectAll );
+extern ABC_DLL bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkSupport( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
+extern ABC_DLL Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
+extern ABC_DLL Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
+extern ABC_DLL Vec_Vec_t * Abc_NtkLevelize( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkLevel( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkLevelReverse( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_AigGetLevelizedOrder( Abc_Ntk_t * pNtk, int fCollectCis );
/*=== abcFanio.c ==========================================================*/
-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 );
-extern int Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin );
+extern ABC_DLL void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern ABC_DLL void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern ABC_DLL void Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
+extern ABC_DLL void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
+extern ABC_DLL Abc_Obj_t * Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type );
+extern ABC_DLL void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
+extern ABC_DLL void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
+extern ABC_DLL int Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin );
/*=== abcFraig.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
-extern void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
-extern Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk );
-extern int Abc_NtkFraigStore( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkFraigRestore();
-extern void Abc_NtkFraigStoreClean();
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
+extern ABC_DLL void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkFraigStore( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFraigRestore();
+extern ABC_DLL void Abc_NtkFraigStoreClean();
/*=== abcFunc.c ==========================================================*/
-extern int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
-extern char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
-extern int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
-extern void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
-extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
-extern void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
-extern int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
-extern int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
-extern int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
-extern int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
-extern int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
-extern int Abc_NtkToAig( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
+extern ABC_DLL char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
+extern ABC_DLL int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern ABC_DLL void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
+extern ABC_DLL int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+extern ABC_DLL void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkMapToSop( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkToSop( Abc_Ntk_t * pNtk, int fDirect );
+extern ABC_DLL int Abc_NtkToBdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkToAig( Abc_Ntk_t * pNtk );
/*=== abcHaig.c ==========================================================*/
-extern int Abc_NtkHaigStart( Abc_Ntk_t * pNtk );
-extern int Abc_NtkHaigStop( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkHaigStart( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkHaigStop( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk );
/*=== abcHie.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFlattenLogicHierarchy( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkConvertBlackboxes( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL );
/*=== abcLatch.c ==========================================================*/
-extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
-extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
-extern int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
-extern Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
-extern void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
-extern Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
-extern void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
+extern ABC_DLL bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
+extern ABC_DLL int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
+extern ABC_DLL Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
+extern ABC_DLL void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
/*=== abcLib.c ==========================================================*/
-extern Abc_Lib_t * Abc_LibCreate( char * pName );
-extern void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
-extern void Abc_LibPrint( Abc_Lib_t * pLib );
-extern int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
-extern int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
-extern Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib );
+extern ABC_DLL Abc_Lib_t * Abc_LibCreate( char * pName );
+extern ABC_DLL void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_LibPrint( Abc_Lib_t * pLib );
+extern ABC_DLL int Abc_LibAddModel( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_LibFindModelByName( Abc_Lib_t * pLib, char * pName );
+extern ABC_DLL int Abc_LibFindTopLevelModels( Abc_Lib_t * pLib );
+extern ABC_DLL Abc_Ntk_t * Abc_LibDeriveRoot( Abc_Lib_t * pLib );
/*=== abcMiter.c ==========================================================*/
-extern int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
-extern int Abc_NodeMinimumBase( Abc_Obj_t * pNode );
-extern int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
-extern int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NodeMinimumBase( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
/*=== abcMiter.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti );
-extern void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
-extern Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
-extern Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
-extern Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
-extern Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
-extern Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
-extern int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
-extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
-extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic, int fMulti );
+extern ABC_DLL void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
+extern ABC_DLL void Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose );
/*=== abcNames.c ====================================================*/
-extern char * Abc_ObjName( Abc_Obj_t * pNode );
-extern char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
-extern char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
-extern char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
-extern void Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void Abc_NtkTrasferNamesNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
-extern Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames );
-extern void Abc_NodeFreeNames( Vec_Ptr_t * vNames );
-extern char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
-extern int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
-extern void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
-extern void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
-extern void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk );
-extern void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
-extern void Abc_NtkShortNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL char * Abc_ObjName( Abc_Obj_t * pNode );
+extern ABC_DLL char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix );
+extern ABC_DLL char * Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
+extern ABC_DLL char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
+extern ABC_DLL void Abc_NtkTrasferNames( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL void Abc_NtkTrasferNamesNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
+extern ABC_DLL Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames );
+extern ABC_DLL void Abc_NodeFreeNames( Vec_Ptr_t * vNames );
+extern ABC_DLL char ** Abc_NtkCollectCioNames( Abc_Ntk_t * pNtk, int fCollectCos );
+extern ABC_DLL int Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern ABC_DLL void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
+extern ABC_DLL void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkShortNames( Abc_Ntk_t * pNtk );
/*=== abcNetlist.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkToLogic( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkToNetlist( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
/*=== abcNtbdd.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
-extern Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
-extern DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
-extern int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
+extern ABC_DLL DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
+extern ABC_DLL DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
+extern ABC_DLL int Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk );
/*=== abcNtk.c ==========================================================*/
-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 void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern Abc_Ntk_t * Abc_NtkStartRead( char * pName );
-extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis );
-extern Abc_Ntk_t * Abc_NtkCreateConeArray( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fUseAllCis );
-extern void Abc_NtkAppendToCone( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots );
-extern Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName );
-extern Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
-extern Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
-extern Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop );
-extern void Abc_NtkDelete( Abc_Ntk_t * pNtk );
-extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
-extern void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern ABC_DLL void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkStartRead( char * pName );
+extern ABC_DLL void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateConeArray( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, int fUseAllCis );
+extern ABC_DLL void Abc_NtkAppendToCone( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop );
+extern ABC_DLL void Abc_NtkDelete( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches );
/*=== 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 Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
-extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
-extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
-extern void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
-extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
-extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
-extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
-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_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
-extern bool Abc_NodeIsConst( Abc_Obj_t * pNode );
-extern bool Abc_NodeIsConst0( Abc_Obj_t * pNode );
-extern bool Abc_NodeIsConst1( Abc_Obj_t * pNode );
-extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode );
-extern bool Abc_NodeIsInv( Abc_Obj_t * pNode );
-extern void Abc_NodeComplement( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern ABC_DLL void Abc_ObjRecycle( Abc_Obj_t * pObj );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern ABC_DLL void Abc_NtkDeleteObj( Abc_Obj_t * pObj );
+extern ABC_DLL void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
+extern ABC_DLL void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj );
+extern ABC_DLL Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern ABC_DLL Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern ABC_DLL bool Abc_NodeIsConst( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsConst0( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsConst1( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsBuf( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsInv( Abc_Obj_t * pNode );
+extern ABC_DLL void Abc_NodeComplement( Abc_Obj_t * pNode );
/*=== abcPrint.c ==========================================================*/
-extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
-extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
-extern void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
-extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
-extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
-extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
-extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
-extern void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
-extern void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
+extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
+extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
+extern ABC_DLL void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
+extern ABC_DLL void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
+extern ABC_DLL void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
+extern ABC_DLL void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
+extern ABC_DLL void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
+extern ABC_DLL void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
/*=== abcProve.c ==========================================================*/
-extern int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
-extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
+extern ABC_DLL int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
+extern ABC_DLL int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
/*=== abcRec.c ==========================================================*/
-extern void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts );
-extern void Abc_NtkRecStop();
-extern void Abc_NtkRecAdd( Abc_Ntk_t * pNtk );
-extern void Abc_NtkRecPs();
-extern void Abc_NtkRecFilter( int iVar, int iPlus );
-extern Abc_Ntk_t * Abc_NtkRecUse();
-extern int Abc_NtkRecIsRunning();
-extern int Abc_NtkRecVarNum();
-extern Vec_Int_t * Abc_NtkRecMemory();
-extern int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
+extern ABC_DLL void Abc_NtkRecStart( Abc_Ntk_t * pNtk, int nVars, int nCuts );
+extern ABC_DLL void Abc_NtkRecStop();
+extern ABC_DLL void Abc_NtkRecAdd( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkRecPs();
+extern ABC_DLL void Abc_NtkRecFilter( int iVar, int iPlus );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkRecUse();
+extern ABC_DLL int Abc_NtkRecIsRunning();
+extern ABC_DLL int Abc_NtkRecVarNum();
+extern ABC_DLL Vec_Int_t * Abc_NtkRecMemory();
+extern ABC_DLL int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTruth, int nVars );
/*=== abcReconv.c ==========================================================*/
-extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
-extern void Abc_NtkManCutStop( Abc_ManCut_t * p );
-extern Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
-extern Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
-extern Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
-extern Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
-extern void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
-extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
-extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
-extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
+extern ABC_DLL Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
+extern ABC_DLL void Abc_NtkManCutStop( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
+extern ABC_DLL Vec_Ptr_t * Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
+extern ABC_DLL void Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
+extern ABC_DLL DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
+extern ABC_DLL DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
+extern ABC_DLL Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
/*=== abcRefs.c ==========================================================*/
-extern int Abc_NodeMffcSize( Abc_Obj_t * pNode );
-extern int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
-extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
-extern int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
-extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
-extern void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
-extern int Abc_NodeDeref_rec( Abc_Obj_t * pNode );
-extern int Abc_NodeRef_rec( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NodeMffcSize( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NodeMffcLabelAig( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NodeMffcLabel( Abc_Obj_t * pNode );
+extern ABC_DLL void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
+extern ABC_DLL int Abc_NodeDeref_rec( Abc_Obj_t * pNode );
+extern ABC_DLL int Abc_NodeRef_rec( Abc_Obj_t * pNode );
/*=== abcRefactor.c ==========================================================*/
-extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
+extern ABC_DLL int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
/*=== abcRewrite.c ==========================================================*/
-extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable );
+extern ABC_DLL int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable );
/*=== abcSat.c ==========================================================*/
-extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
-extern void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
+extern ABC_DLL int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
+extern ABC_DLL void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
/*=== abcSop.c ==========================================================*/
-extern char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
-extern char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
-extern char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
-extern char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
-extern char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
-extern char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
-extern char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
-extern char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
-extern char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
-extern char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
-extern char * Abc_SopCreateMux( Extra_MmFlex_t * pMan );
-extern char * Abc_SopCreateInv( Extra_MmFlex_t * pMan );
-extern char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
-extern char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
-extern char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover );
-extern int Abc_SopGetCubeNum( char * pSop );
-extern int Abc_SopGetLitNum( char * pSop );
-extern int Abc_SopGetVarNum( char * pSop );
-extern int Abc_SopGetPhase( char * pSop );
-extern int Abc_SopGetIthCareLit( char * pSop, int i );
-extern void Abc_SopComplement( char * pSop );
-extern bool Abc_SopIsComplement( char * pSop );
-extern bool Abc_SopIsConst0( char * pSop );
-extern bool Abc_SopIsConst1( char * pSop );
-extern bool Abc_SopIsBuf( char * pSop );
-extern bool Abc_SopIsInv( char * pSop );
-extern bool Abc_SopIsAndType( char * pSop );
-extern bool Abc_SopIsOrType( char * pSop );
-extern int Abc_SopIsExorType( char * pSop );
-extern bool Abc_SopCheck( char * pSop, int nFanins );
-extern char * Abc_SopFromTruthBin( char * pTruth );
-extern char * Abc_SopFromTruthHex( char * pTruth );
-extern char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues );
-extern char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues );
-extern char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
-extern char * Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
+extern ABC_DLL char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
+extern ABC_DLL char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
+extern ABC_DLL char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
+extern ABC_DLL char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
+extern ABC_DLL char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
+extern ABC_DLL char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
+extern ABC_DLL char * Abc_SopCreateMux( Extra_MmFlex_t * pMan );
+extern ABC_DLL char * Abc_SopCreateInv( Extra_MmFlex_t * pMan );
+extern ABC_DLL char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
+extern ABC_DLL char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
+extern ABC_DLL char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover );
+extern ABC_DLL int Abc_SopGetCubeNum( char * pSop );
+extern ABC_DLL int Abc_SopGetLitNum( char * pSop );
+extern ABC_DLL int Abc_SopGetVarNum( char * pSop );
+extern ABC_DLL int Abc_SopGetPhase( char * pSop );
+extern ABC_DLL int Abc_SopGetIthCareLit( char * pSop, int i );
+extern ABC_DLL void Abc_SopComplement( char * pSop );
+extern ABC_DLL bool Abc_SopIsComplement( char * pSop );
+extern ABC_DLL bool Abc_SopIsConst0( char * pSop );
+extern ABC_DLL bool Abc_SopIsConst1( char * pSop );
+extern ABC_DLL bool Abc_SopIsBuf( char * pSop );
+extern ABC_DLL bool Abc_SopIsInv( char * pSop );
+extern ABC_DLL bool Abc_SopIsAndType( char * pSop );
+extern ABC_DLL bool Abc_SopIsOrType( char * pSop );
+extern ABC_DLL int Abc_SopIsExorType( char * pSop );
+extern ABC_DLL bool Abc_SopCheck( char * pSop, int nFanins );
+extern ABC_DLL char * Abc_SopFromTruthBin( char * pTruth );
+extern ABC_DLL char * Abc_SopFromTruthHex( char * pTruth );
+extern ABC_DLL char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues );
+extern ABC_DLL char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues );
+extern ABC_DLL char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
+extern ABC_DLL char * Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
/*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
-extern Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
-extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
-extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
+extern ABC_DLL Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
+extern ABC_DLL int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
+extern ABC_DLL Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
/*=== abcSweep.c ==========================================================*/
-extern int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
-extern int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
-extern int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fVerbose );
+extern ABC_DLL int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
+extern ABC_DLL int Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
+extern ABC_DLL int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fLatchSweep, int fAutoSweep, int fVerbose );
/*=== abcTiming.c ==========================================================*/
-extern Abc_Time_t * Abc_NodeReadArrival( Abc_Obj_t * pNode );
-extern Abc_Time_t * Abc_NodeReadRequired( Abc_Obj_t * pNode );
-extern Abc_Time_t * Abc_NtkReadDefaultArrival( Abc_Ntk_t * pNtk );
-extern Abc_Time_t * Abc_NtkReadDefaultRequired( Abc_Ntk_t * pNtk );
-extern void Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float Rise, float Fall );
-extern void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall );
-extern void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
-extern void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
-extern void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk );
-extern void Abc_ManTimeStop( Abc_ManTime_t * p );
-extern void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
-extern void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
-extern float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
-extern Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
-extern float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
-extern int Abc_ObjLevelNew( Abc_Obj_t * pObj );
-extern int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj );
-extern int Abc_ObjRequiredLevel( Abc_Obj_t * pObj );
-extern int Abc_ObjReverseLevel( Abc_Obj_t * pObj );
-extern void Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
-extern void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease );
-extern void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
-extern void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-extern void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL Abc_Time_t * Abc_NodeReadArrival( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Time_t * Abc_NodeReadRequired( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Time_t * Abc_NtkReadDefaultArrival( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Time_t * Abc_NtkReadDefaultRequired( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float Rise, float Fall );
+extern ABC_DLL void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall );
+extern ABC_DLL void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
+extern ABC_DLL void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
+extern ABC_DLL void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_ManTimeStop( Abc_ManTime_t * p );
+extern ABC_DLL void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
+extern ABC_DLL void Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
+extern ABC_DLL float * Abc_NtkGetCiArrivalFloats( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Time_t * Abc_NtkGetCiArrivalTimes( Abc_Ntk_t * pNtk );
+extern ABC_DLL float Abc_NtkDelayTrace( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_ObjLevelNew( Abc_Obj_t * pObj );
+extern ABC_DLL int Abc_ObjReverseLevelNew( Abc_Obj_t * pObj );
+extern ABC_DLL int Abc_ObjRequiredLevel( Abc_Obj_t * pObj );
+extern ABC_DLL int Abc_ObjReverseLevel( Abc_Obj_t * pObj );
+extern ABC_DLL void Abc_ObjSetReverseLevel( Abc_Obj_t * pObj, int LevelR );
+extern ABC_DLL void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk, int nMaxLevelIncrease );
+extern ABC_DLL void Abc_NtkStopReverseLevels( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
+extern ABC_DLL void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
/*=== abcUtil.c ==========================================================*/
-extern void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan );
-extern void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
-extern void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk );
-extern double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
-extern int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
-extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
-extern void Abc_NtkCleanData( Abc_Ntk_t * pNtk );
-extern void Abc_NtkCleanEquiv( Abc_Ntk_t * pNtk );
-extern int Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
-extern void Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );
-extern void Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
-extern void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t * Abc_NodeFindCoFanout( Abc_Obj_t * pNode );
-extern Abc_Obj_t * Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode );
-extern Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
-extern bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
-extern int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
-extern void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode );
-extern bool Abc_NodeIsExorType( Abc_Obj_t * pNode );
-extern bool Abc_NodeIsMuxType( Abc_Obj_t * pNode );
-extern bool Abc_NodeIsMuxControlType( Abc_Obj_t * pNode );
-extern Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE );
-extern int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
-extern void Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
-extern Vec_Ptr_t * Abc_NtkCollectLatches( Abc_Ntk_t * pNtk );
-extern int Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
-extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
-extern Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
-extern void Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
-extern int Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
-extern void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void * Abc_NtkAttrFree( Abc_Ntk_t * pNtk, int Attr, int fFreeMan );
+extern ABC_DLL void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetCubePairNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetBddNodeNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL double Abc_NtkGetMappedArea( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkCleanData( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkCleanEquiv( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );
+extern ABC_DLL void Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
+extern ABC_DLL Abc_Obj_t * Abc_NodeFindCoFanout( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t * Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t * Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
+extern ABC_DLL void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsExorType( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsMuxType( Abc_Obj_t * pNode );
+extern ABC_DLL bool Abc_NodeIsMuxControlType( Abc_Obj_t * pNode );
+extern ABC_DLL Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE );
+extern ABC_DLL int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 );
+extern ABC_DLL void Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkCollectLatches( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern ABC_DLL int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
+extern ABC_DLL Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
+extern ABC_DLL Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
+extern ABC_DLL int Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
+extern ABC_DLL void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
/*=== abcVerify.c ==========================================================*/
-extern int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
-extern int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
+extern ABC_DLL int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
+extern ABC_DLL int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
#ifdef __cplusplus
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0437f8a9..9b5ebddb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -91,6 +91,7 @@ static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDFrames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -181,6 +182,7 @@ static int Abc_CommandFlowRetime ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweepTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -345,6 +347,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "andpos", Abc_CommandAndPos, 1 );
Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 );
Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "dframes", Abc_CommandDFrames, 1 );
Cmd_CommandAdd( pAbc, "Various", "sop", Abc_CommandSop, 0 );
Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 );
Cmd_CommandAdd( pAbc, "Various", "aig", Abc_CommandAig, 0 );
@@ -432,6 +435,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "testssw", Abc_CommandSeqSweepTest, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "lcorr", Abc_CommandLcorr, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
@@ -5071,8 +5075,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes;
- int fInitial;
int nFrames;
+ int fInitial;
+ int fVerbose;
int c;
pNtk = Abc_FrameReadNtk(pAbc);
@@ -5080,10 +5085,11 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fInitial = 0;
nFrames = 5;
+ fInitial = 0;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fih" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
{
switch ( c )
{
@@ -5101,6 +5107,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'i':
fInitial ^= 1;
break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -5118,11 +5127,11 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
- pNtkRes = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
+ pNtkRes = Abc_NtkFrames( pNtkTemp, nFrames, fInitial, fVerbose );
Abc_NtkDelete( pNtkTemp );
}
else
- pNtkRes = Abc_NtkFrames( pNtk, nFrames, fInitial );
+ pNtkRes = Abc_NtkFrames( pNtk, nFrames, fInitial, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Unrolling the network has failed.\n" );
@@ -5133,15 +5142,129 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: frames [-F num] [-ih]\n" );
+ fprintf( pErr, "usage: frames [-F num] [-ivh]\n" );
fprintf( pErr, "\t unrolls the network for a number of time frames\n" );
fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames );
fprintf( pErr, "\t-i : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" );
+ fprintf( pErr, "\t-v : toggles outputting verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandDFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes;
+ int nPrefix;
+ int nFrames;
+ int fInitial;
+ int fVerbose;
+ int c;
+
+ extern Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInitial, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nPrefix = 5;
+ nFrames = 5;
+ fInitial = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NFivh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nPrefix = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nPrefix <= 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames <= 0 )
+ goto usage;
+ break;
+ case 'i':
+ fInitial ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( nPrefix > nFrames )
+ {
+ fprintf( pErr, "Prefix (%d) cannot be more than the number of frames (%d).\n", nPrefix, nFrames );
+ return 1;
+ }
+
+ // get the new network
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ pNtkTemp = Abc_NtkStrash( pNtk, 0, 0, 0 );
+ pNtkRes = Abc_NtkDarFrames( pNtkTemp, nPrefix, nFrames, fInitial, fVerbose );
+ Abc_NtkDelete( pNtkTemp );
+ }
+ else
+ pNtkRes = Abc_NtkDarFrames( pNtk, nPrefix, nFrames, fInitial, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Unrolling the network has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: dframes [-NF num] [-ivh]\n" );
+ fprintf( pErr, "\t unrolls the network with simplification\n" );
+ fprintf( pErr, "\t-N num : the number of frames to use as prefix [default = %d]\n", nPrefix );
+ fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-i : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" );
+ fprintf( pErr, "\t-v : toggles outputting verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
+
/**Function*************************************************************
Synopsis []
@@ -7352,6 +7475,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
+ extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
@@ -7537,6 +7661,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
*/
// Abc_NtkDarPartition( pNtk );
+Abc_NtkDarTest( pNtk );
+return 0;
pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
if ( pNtkRes == NULL )
@@ -12891,6 +13017,170 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandSeqSweepTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ char * pFileName;
+ Fra_Ssw_t Pars, * pPars = &Pars;
+ int c;
+// extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars );
+ extern int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams );
+
+ // set defaults
+ pPars->nPartSize = 0;
+ pPars->nOverSize = 0;
+ pPars->nFramesP = 0;
+ pPars->nFramesK = 1;
+ pPars->nMaxImps = 5000;
+ pPars->nMaxLevs = 0;
+ pPars->fUseImps = 0;
+ pPars->fRewrite = 0;
+ pPars->fFraiging = 0;
+ pPars->fLatchCorr = 0;
+ pPars->fWriteImps = 0;
+ pPars->fUse1Hot = 0;
+ pPars->fVerbose = 0;
+ pPars->TimeLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nPartSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nPartSize < 2 )
+ goto usage;
+ break;
+ case 'Q':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nOverSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nOverSize < 0 )
+ goto usage;
+ break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nFramesP = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFramesP < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nFramesK = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFramesK <= 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxImps = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxImps <= 0 )
+ goto usage;
+ break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxLevs <= 0 )
+ goto usage;
+ break;
+ case 'i':
+ pPars->fUseImps ^= 1;
+ break;
+ case 'r':
+ pPars->fRewrite ^= 1;
+ break;
+ case 'f':
+ pPars->fFraiging ^= 1;
+ break;
+ case 'l':
+ pPars->fLatchCorr ^= 1;
+ break;
+ case 'e':
+ pPars->fWriteImps ^= 1;
+ break;
+ case 't':
+ pPars->fUse1Hot ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ // get the input file name
+ if ( argc == globalUtilOptind + 1 )
+ pFileName = argv[globalUtilOptind];
+ else
+ {
+ printf( "File name should be given on the command line.\n" );
+ return 1;
+ }
+ Fra_FraigInductionTest( pFileName, pPars );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: testssw [-PQNFL num] [-lrfetvh] <file>\n" );
+ fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
+ fprintf( stdout, "\t (outputs a file with a set of pairs of equivalent nodes)\n" );
+ fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
+ fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
+ fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
+ fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
+ fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
+// fprintf( stdout, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps );
+// fprintf( stdout, "\t-i : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" );
+ fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
+ fprintf( stdout, "\t-r : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" );
+ fprintf( stdout, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" );
+ fprintf( stdout, "\t-e : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" );
+ fprintf( stdout, "\t-t : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 7b7617e6..ca54e4e1 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1491,6 +1491,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
+
pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@@ -2083,6 +2084,38 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
/**Function*************************************************************
+ Synopsis [Performs phase abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
+ pMan = Abc_NtkToDar( pNtk, 0, 0 );
+ pMan->nRegs = Abc_NtkLatchNum(pNtk);
+ pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+ pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+ if ( pMan == NULL )
+ return NULL;
+ pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
+ Aig_ManStop( pTemp );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs BDD-based reachability analysis.]
Description []
@@ -2107,6 +2140,38 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
}
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
+{
+ Aig_Man_t * pMan;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ pMan->nRegs = Abc_NtkLatchNum(pNtk);
+ pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+ pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+ if ( pMan == NULL )
+ return;
+
+Aig_ManSetRegNum( pMan, pMan->nRegs );
+Aig_ManPrintStats( pMan );
+Saig_ManDumpBlif( pMan, "_temp_.blif" );
+Aig_ManStop( pMan );
+pMan = Saig_ManReadBlif( "_temp_.blif" );
+Aig_ManPrintStats( pMan );
+
+ Aig_ManStop( pMan );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 9bab238b..4e1022b8 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -766,7 +766,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
+Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose )
{
char Buffer[1000];
ProgressBar * pProgress;
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 328d2907..96a4566d 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -478,7 +478,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
}
// create the timeframes
- pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
+ pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
Abc_NtkDelete( pMiter );
if ( pFrames == NULL )
{
@@ -564,7 +564,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
}
// create the timeframes
- pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
+ pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
Abc_NtkDelete( pMiter );
if ( pFrames == NULL )
{
@@ -777,7 +777,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
Vec_Ptr_t * vSupp;
int i, k;
// get the timeframes of the network
- pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 );
+ pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0, 0 );
//Abc_NtkShowAig( pFrames );
// get the PO of the timeframes
diff --git a/src/base/main/main.h b/src/base/main/main.h
index b5cc0dfe..852b8f25 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: main.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: main.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
***********************************************************************/
@@ -69,47 +69,57 @@ typedef struct Abc_Frame_t_ Abc_Frame_t;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
/*=== main.c ===========================================================*/
-extern void Abc_Start();
-extern void Abc_Stop();
+extern ABC_DLL void Abc_Start();
+extern ABC_DLL void Abc_Stop();
/*=== mainFrame.c ===========================================================*/
-extern Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p );
-extern FILE * Abc_FrameReadOut( Abc_Frame_t * p );
-extern FILE * Abc_FrameReadErr( Abc_Frame_t * p );
-extern bool Abc_FrameReadMode( Abc_Frame_t * p );
-extern bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
-extern void Abc_FrameRestart( Abc_Frame_t * p );
-extern bool Abc_FrameShowProgress( Abc_Frame_t * p );
-
-extern void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
-extern void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
-extern void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
-extern void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
-extern void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
-
-extern void Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
-extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
-
-extern Vec_Ptr_t * Abc_FrameReadStore();
-extern int Abc_FrameReadStoreSize();
-extern void * Abc_FrameReadLibLut();
-extern void * Abc_FrameReadLibGen();
-extern void * Abc_FrameReadLibSuper();
-extern void * Abc_FrameReadLibVer();
-extern void * Abc_FrameReadManDd();
-extern void * Abc_FrameReadManDec();
-extern char * Abc_FrameReadFlag( char * pFlag );
-extern bool Abc_FrameIsFlagEnabled( char * pFlag );
-
-extern void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk );
-extern void Abc_FrameSetNtkStoreSize( int nStored );
-extern void Abc_FrameSetLibLut( void * pLib );
-extern void Abc_FrameSetLibGen( void * pLib );
-extern void Abc_FrameSetLibSuper( void * pLib );
-extern void Abc_FrameSetLibVer( void * pLib );
-extern void Abc_FrameSetFlag( char * pFlag, char * pValue );
+extern ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p );
+extern ABC_DLL FILE * Abc_FrameReadOut( Abc_Frame_t * p );
+extern ABC_DLL FILE * Abc_FrameReadErr( Abc_Frame_t * p );
+extern ABC_DLL bool Abc_FrameReadMode( Abc_Frame_t * p );
+extern ABC_DLL bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
+extern ABC_DLL void Abc_FrameRestart( Abc_Frame_t * p );
+extern ABC_DLL bool Abc_FrameShowProgress( Abc_Frame_t * p );
+
+extern ABC_DLL void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
+extern ABC_DLL void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
+extern ABC_DLL void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
+extern ABC_DLL void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
+extern ABC_DLL void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
+
+extern ABC_DLL void Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
+extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame();
+
+extern ABC_DLL Vec_Ptr_t * Abc_FrameReadStore();
+extern ABC_DLL int Abc_FrameReadStoreSize();
+extern ABC_DLL void * Abc_FrameReadLibLut();
+extern ABC_DLL void * Abc_FrameReadLibGen();
+extern ABC_DLL void * Abc_FrameReadLibSuper();
+extern ABC_DLL void * Abc_FrameReadLibVer();
+extern ABC_DLL void * Abc_FrameReadManDd();
+extern ABC_DLL void * Abc_FrameReadManDec();
+extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag );
+extern ABC_DLL bool Abc_FrameIsFlagEnabled( char * pFlag );
+
+extern ABC_DLL void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk );
+extern ABC_DLL void Abc_FrameSetNtkStoreSize( int nStored );
+extern ABC_DLL void Abc_FrameSetLibLut( void * pLib );
+extern ABC_DLL void Abc_FrameSetLibGen( void * pLib );
+extern ABC_DLL void Abc_FrameSetLibSuper( void * pLib );
+extern ABC_DLL void Abc_FrameSetLibVer( void * pLib );
+extern ABC_DLL void Abc_FrameSetFlag( char * pFlag, char * pValue );
#ifdef __cplusplus
}
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index f79f9126..b03a00fa 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -14,13 +14,13 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: mainInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
***********************************************************************/
#ifndef __MAIN_INT_H__
#define __MAIN_INT_H__
-
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -93,21 +93,31 @@ struct Abc_Frame_t_
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#ifdef WIN32
+#define DLLEXPORT __declspec(dllexport)
+#define DLLIMPORT __declspec(dllimport)
+#else /* defined(WIN32) */
+#define DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL DLLIMPORT
+#endif
/*=== mvMain.c ===========================================================*/
-extern int main( int argc, char * argv[] );
+extern ABC_DLL int main( int argc, char * argv[] );
/*=== mvInit.c ===================================================*/
-extern void Abc_FrameInit( Abc_Frame_t * pAbc );
-extern void Abc_FrameEnd( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_FrameInit( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_FrameEnd( Abc_Frame_t * pAbc );
/*=== mvFrame.c =====================================================*/
-extern Abc_Frame_t * Abc_FrameAllocate();
-extern void Abc_FrameDeallocate( Abc_Frame_t * p );
+extern ABC_DLL Abc_Frame_t * Abc_FrameAllocate();
+extern ABC_DLL void Abc_FrameDeallocate( Abc_Frame_t * p );
/*=== mvUtils.c =====================================================*/
-extern char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
-extern char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
-extern void Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
-extern void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
-extern void Abc_UtilsSource( Abc_Frame_t * pAbc );
+extern ABC_DLL char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
+extern ABC_DLL char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
+extern ABC_DLL void Abc_UtilsSource( Abc_Frame_t * pAbc );
#endif
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 4091ac7f..ee82fc3e 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -72,6 +72,10 @@ typedef long long sint64;
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#endif
+#ifndef CALLOC
+#define CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
+#endif
+
#ifndef FREE
#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 08:10:37 +0000