diff options
Diffstat (limited to 'src/aig/saig')
| -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 |
4 files changed, 829 insertions, 1 deletions
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 /// +//////////////////////////////////////////////////////////////////////// + + |