diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/aig/aig.h | 3 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 19 | ||||
-rw-r--r-- | src/aig/aig/aigUtil.c | 22 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 1 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 57 | ||||
-rw-r--r-- | src/aig/ntl/ntl.h | 164 | ||||
-rw-r--r-- | src/aig/nwk/nwk.h | 136 | ||||
-rw-r--r-- | src/aig/saig/module.make | 4 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 5 | ||||
-rw-r--r-- | src/aig/saig/saigIoa.c | 399 | ||||
-rw-r--r-- | src/aig/saig/saigTrans.c | 422 |
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 /// +//////////////////////////////////////////////////////////////////////// + + |