summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-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
11 files changed, 1092 insertions, 140 deletions
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 ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-20 12:33:58 +0000