diff options
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saig.h | 82 | ||||
| -rw-r--r-- | src/aig/saig/saigPhase.c | 763 | ||||
| -rw-r--r-- | src/aig/saig/saig_.c | 47 |
3 files changed, 892 insertions, 0 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h new file mode 100644 index 00000000..ce09fd32 --- /dev/null +++ b/src/aig/saig/saig.h @@ -0,0 +1,82 @@ +/**CFile**************************************************************** + + FileName [saig.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __SAIG_H__ +#define __SAIG_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Saig_ManPiNum( Aig_Man_t * p ) { return p->nTruePis; } +static inline int Saig_ManPoNum( Aig_Man_t * p ) { return p->nTruePos; } +static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; } +static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i); } +static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i); } + +// iterator over the primary inputs/outputs +#define Saig_ManForEachPi( p, pObj, i ) \ + Vec_PtrForEachEntryStop( p->vPis, pObj, i, Saig_ManPiNum(p) ) +#define Saig_ManForEachPo( p, pObj, i ) \ + Vec_PtrForEachEntryStop( p->vPos, pObj, i, Saig_ManPoNum(p) ) +// iterator over the latch inputs/outputs +#define Saig_ManForEachLo( p, pObj, i ) \ + for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = Vec_PtrEntry(p->vPis, i+Saig_ManPiNum(p))), 1); i++ ) +#define Saig_ManForEachLi( p, pObj, i ) \ + for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = Vec_PtrEntry(p->vPos, i+Saig_ManPoNum(p))), 1); i++ ) +// iterator over the latch input and outputs +#define Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) \ + for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1) \ + && (((pObjLo)=Saig_ManLo(p, i)), 1); i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== saigPhase.c ==========================================================*/ + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c new file mode 100644 index 00000000..f83666c4 --- /dev/null +++ b/src/aig/saig/saigPhase.c @@ -0,0 +1,763 @@ +/**CFile**************************************************************** + + FileName [saigPhase.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Automated phase abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigPhase.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +/* + The algorithm is described in the paper: Per Bjesse and Jim Kukula, + "Automatic Phase Abstraction for Formal Verification", ICCAD 2005 + http://www.iccad.com/data2/iccad/iccad_05acceptedpapers.nsf/9cfb1ebaaf59043587256a6a00031f78/1701ecf34b149e958725702f00708828?OpenDocument +*/ + +// the maximum number of cycles of termiry simulation +#define TSIM_MAX_ROUNDS 10000 +#define TSIM_ONE_SERIES 3000 + +#define SAIG_XVS0 1 +#define SAIG_XVS1 2 +#define SAIG_XVSX 3 + +static inline int Saig_XsimConvertValue( int v ) { return v == 0? SAIG_XVS0 : (v == 1? SAIG_XVS1 : (v == 2? SAIG_XVSX : -1)); } + +static inline void Saig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; } +static inline int Saig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; } +static inline int Saig_XsimInv( int Value ) +{ + if ( Value == SAIG_XVS0 ) + return SAIG_XVS1; + if ( Value == SAIG_XVS1 ) + return SAIG_XVS0; + assert( Value == SAIG_XVSX ); + return SAIG_XVSX; +} +static inline int Saig_XsimAnd( int Value0, int Value1 ) +{ + if ( Value0 == SAIG_XVS0 || Value1 == SAIG_XVS0 ) + return SAIG_XVS0; + if ( Value0 == SAIG_XVSX || Value1 == SAIG_XVSX ) + return SAIG_XVSX; + assert( Value0 == SAIG_XVS1 && Value1 == SAIG_XVS1 ); + return SAIG_XVS1; +} +static inline int Saig_XsimRand2() +{ + return (rand() & 1) ? SAIG_XVS1 : SAIG_XVS0; +} +static inline int Saig_XsimRand3() +{ + int RetValue; + do { + RetValue = rand() & 3; + } while ( RetValue == 0 ); + return RetValue; +} +static inline int Saig_ObjGetXsimFanin0( Aig_Obj_t * pObj ) +{ + int RetValue; + RetValue = Saig_ObjGetXsim(Aig_ObjFanin0(pObj)); + return Aig_ObjFaninC0(pObj)? Saig_XsimInv(RetValue) : RetValue; +} +static inline int Saig_ObjGetXsimFanin1( Aig_Obj_t * pObj ) +{ + int RetValue; + RetValue = Saig_ObjGetXsim(Aig_ObjFanin1(pObj)); + return Aig_ObjFaninC1(pObj)? Saig_XsimInv(RetValue) : RetValue; +} +static inline void Saig_XsimPrint( FILE * pFile, int Value ) +{ + if ( Value == SAIG_XVS0 ) + { + fprintf( pFile, "0" ); + return; + } + if ( Value == SAIG_XVS1 ) + { + fprintf( pFile, "1" ); + return; + } + assert( Value == SAIG_XVSX ); + fprintf( pFile, "x" ); +} + +// simulation manager +typedef struct Saig_Tsim_t_ Saig_Tsim_t; +struct Saig_Tsim_t_ +{ + Aig_Man_t * pAig; // the original AIG manager + int nWords; // the number of words in the states + // ternary state representation + Vec_Ptr_t * vStates; // the collection of ternary states + Aig_MmFixed_t * pMem; // memory for ternary states + int nPrefix; // prefix of the ternary state space + int nCycle; // cycle of the ternary state space + int nNonXRegs; // the number of candidate registers + Vec_Int_t * vNonXRegs; // the candidate registers + // hash table for terminary states + unsigned ** pBins; + int nBins; +}; + +static inline unsigned * Saig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); } +static inline void Saig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; } + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig ) +{ + Saig_Tsim_t * p; + p = (Saig_Tsim_t *)malloc( sizeof(Saig_Tsim_t) ); + memset( p, 0, sizeof(Saig_Tsim_t) ); + p->pAig = pAig; + p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) ); + p->vStates = Vec_PtrAlloc( 1000 ); + p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 ); + p->nBins = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2); + p->pBins = ALLOC( unsigned *, p->nBins ); + memset( p->pBins, 0, sizeof(unsigned *) * p->nBins ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deallocates simulation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_TsiStop( Saig_Tsim_t * p ) +{ + if ( p->vNonXRegs ) + Vec_IntFree( p->vNonXRegs ); + Aig_MmFixedStop( p->pMem, 0 ); + Vec_PtrFree( p->vStates ); + free( p->pBins ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Computes hash value of the node using its simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize ) +{ + static int s_FPrimes[128] = { + 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, + 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, + 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, + 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, + 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, + 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, + 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, + 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, + 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, + 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, + 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, + 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, + 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147 + }; + unsigned uHash; + int i; + uHash = 0; + for ( i = 0; i < nWords; i++ ) + uHash ^= pState[i] * s_FPrimes[i & 0x7F]; + return uHash % nTableSize; +} + +/**Function************************************************************* + + Synopsis [Count non-X-valued registers in the simulation data.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords ) +{ + unsigned * pState; + int nRegs = p->pAig->nRegs; + int Value, i, k; + assert( p->vNonXRegs == NULL ); + p->vNonXRegs = Vec_IntAlloc( 10 ); + for ( i = 0; i < nRegs; i++ ) + { + Vec_PtrForEachEntry( p->vStates, pState, k ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + assert( Value != 0 ); + if ( Value == SAIG_XVSX ) + break; + } + if ( k == Vec_PtrSize(p->vStates) ) + Vec_IntPush( p->vNonXRegs, i ); + } + return Vec_IntSize(p->vNonXRegs); +} + +/**Function************************************************************* + + Synopsis [Count non-X-valued registers in the simulation data.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix ) +{ + unsigned * pState; + int nRegs = p->pAig->nRegs; + int Value, i, k, Counter = 0; + if ( Vec_PtrSize(p->vStates) > 80 ) + return; + for ( i = 0; i < nRegs; i++ ) + { + Vec_PtrForEachEntry( p->vStates, pState, k ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + if ( Value == SAIG_XVSX ) + break; + } + if ( k == Vec_PtrSize(p->vStates) ) + Counter++; + else + continue; + // print trace + printf( "%5d : %5d ", Counter, i ); + Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + if ( Value == SAIG_XVS0 ) + printf( "0" ); + else if ( Value == SAIG_XVS1 ) + printf( "1" ); + else if ( Value == SAIG_XVSX ) + printf( "x" ); + else + assert( 0 ); + if ( k == nPrefix - 1 ) + printf( " " ); + } + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Returns the number of the state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_TsiComputePrefix( Saig_Tsim_t * p, unsigned * pState, int nWords ) +{ + unsigned * pEntry, * pPrev; + int Hash, i; + Hash = Saig_TsiStateHash( pState, nWords, p->nBins ); + for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) ) + if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) ) + { + Vec_PtrForEachEntry( p->vStates, pPrev, i ) + { + if ( pPrev == pEntry ) + return i; + } + assert( 0 ); + return -1; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Checks if the value exists in the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_TsiStateLookup( Saig_Tsim_t * p, unsigned * pState, int nWords ) +{ + unsigned * pEntry; + int Hash; + Hash = Saig_TsiStateHash( pState, nWords, p->nBins ); + for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) ) + if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_TsiStateInsert( Saig_Tsim_t * p, unsigned * pState, int nWords ) +{ + int Hash = Saig_TsiStateHash( pState, nWords, p->nBins ); + assert( !Saig_TsiStateLookup( p, pState, nWords ) ); + Saig_TsiSetNext( pState, nWords, p->pBins[Hash] ); + p->pBins[Hash] = pState; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Saig_TsiStateNew( Saig_Tsim_t * p ) +{ + unsigned * pState; + pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem ); + memset( pState, 0, sizeof(unsigned) * p->nWords ); + Vec_PtrPush( p->vStates, pState ); + return pState; +} + +/**Function************************************************************* + + Synopsis [Inserts value into the table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_TsiStatePrint( Saig_Tsim_t * p, unsigned * pState ) +{ + int i, Value, nZeros = 0, nOnes = 0, nDcs = 0; + for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + if ( Value == SAIG_XVS0 ) + printf( "0" ), nZeros++; + else if ( Value == SAIG_XVS1 ) + printf( "1" ), nOnes++; + else if ( Value == SAIG_XVSX ) + printf( "x" ), nDcs++; + else + assert( 0 ); + } + printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs ); +} + +/**Function************************************************************* + + Synopsis [Count constant values in the state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_TsiStateCount( Saig_Tsim_t * p, unsigned * pState ) +{ + Aig_Obj_t * pObjLi, * pObjLo; + int i, Value, nCounter = 0; + Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i ) + { + Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + nCounter += (Value == SAIG_XVS0 || Value == SAIG_XVS1); + } + return nCounter; +} + +/**Function************************************************************* + + Synopsis [Count constant values in the state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_TsiStateOrAll( Saig_Tsim_t * pTsi, unsigned * pState ) +{ + unsigned * pPrev; + int i, k; + Vec_PtrForEachEntry( pTsi->vStates, pPrev, i ) + { + for ( k = 0; k < pTsi->nWords; k++ ) + pState[k] |= pPrev[k]; + } +} + +/**Function************************************************************* + + Synopsis [Cycles the circuit to create a new initial state.] + + Description [Simulates the circuit with random input for the given + number of timeframes to get a better initial state.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits ) +{ + Saig_Tsim_t * pTsi; + Aig_Obj_t * pObj, * pObjLi, * pObjLo; + unsigned * pState; + int i, f, Value, nCounter; + // allocate the simulation manager + pTsi = Saig_TsiStart( p ); + // initialize the values + Saig_ObjSetXsim( Aig_ManConst1(p), SAIG_XVS1 ); + Saig_ManForEachPi( p, pObj, i ) + Saig_ObjSetXsim( pObj, SAIG_XVSX ); + if ( vInits ) + { + Saig_ManForEachLo( p, pObj, i ) + Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) ); + } + else + { + Saig_ManForEachLo( p, pObj, i ) + Saig_ObjSetXsim( pObj, SAIG_XVS0 ); + } + // simulate for the given number of timeframes + for ( f = 0; f < TSIM_MAX_ROUNDS; f++ ) + { + // collect this state + pState = Saig_TsiStateNew( pTsi ); + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + { + Value = Saig_ObjGetXsim(pObjLo); + if ( Value & 1 ) + Aig_InfoSetBit( pState, 2 * i ); + if ( Value & 2 ) + Aig_InfoSetBit( pState, 2 * i + 1 ); + } +// printf( "%d ", Saig_TsiStateCount(pTsi, pState) ); +// Saig_TsiStatePrint( pTsi, pState ); + // check if this state exists + if ( Saig_TsiStateLookup( pTsi, pState, pTsi->nWords ) ) + return pTsi; + // insert this state + Saig_TsiStateInsert( pTsi, pState, pTsi->nWords ); + // simulate internal nodes + Aig_ManForEachNode( p, pObj, i ) + Saig_ObjSetXsim( pObj, Saig_XsimAnd(Saig_ObjGetXsimFanin0(pObj), Saig_ObjGetXsimFanin1(pObj)) ); + // transfer the latch values + Saig_ManForEachLi( p, pObj, i ) + Saig_ObjSetXsim( pObj, Saig_ObjGetXsimFanin0(pObj) ); + nCounter = 0; + Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) + { + if ( f < TSIM_ONE_SERIES ) + Saig_ObjSetXsim( pObjLo, Saig_ObjGetXsim(pObjLi) ); + else + { + if ( Saig_ObjGetXsim(pObjLi) != Saig_ObjGetXsim(pObjLo) ) + Saig_ObjSetXsim( pObjLo, SAIG_XVSX ); + } + nCounter += (Saig_ObjGetXsim(pObjLo) == SAIG_XVS0); + } + } + printf( "Saig_ManReachableTernary(): Did not reach a fixed point after %d iterations (not a bug).\n", TSIM_MAX_ROUNDS ); + Saig_TsiStop( pTsi ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Finds the registers to phase-abstract.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose ) +{ + int Values[256]; + unsigned * pState; + int r, i, k, Reg, Value; + int nTests = pTsi->nPrefix + 2 * pTsi->nCycle; + assert( nFrames < 256 ); + r = 0; + Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i ) + { + for ( k = 0; k < nTests; k++ ) + { + if ( k < pTsi->nPrefix + pTsi->nCycle ) + pState = Vec_PtrEntry( pTsi->vStates, k ); + else + pState = Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle ); + Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg ); + assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); + if ( k < nFrames || (fIgnore && k == nFrames) ) + Values[k % nFrames] = Value; + else if ( Values[k % nFrames] != Value ) + break; + } + if ( k < nTests ) + continue; + // skip stuck at + if ( fIgnore ) + { + for ( k = 1; k < nFrames; k++ ) + if ( Values[k] != Values[0] ) + break; + if ( k == nFrames ) + continue; + } + // report useful register + Vec_IntWriteEntry( pTsi->vNonXRegs, r++, Reg ); + if ( fVerbose ) + { + printf( "Register %5d has generator: [", Reg ); + for ( k = 0; k < nFrames; k++ ) + Saig_XsimPrint( stdout, Values[k] ); + printf( "]\n" ); + } + } + Vec_IntShrink( pTsi->vNonXRegs, r ); + if ( fVerbose ) + printf( "Found %3d useful registers.\n", Vec_IntSize(pTsi->vNonXRegs) ); + return Vec_IntSize(pTsi->vNonXRegs); +} + +/**Function************************************************************* + + Synopsis [Mapping of AIG nodes into frames nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Aig_Obj_t * Saig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; } +static inline void Saig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; } + +static inline Aig_Obj_t * Saig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Saig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } + +/**Function************************************************************* + + Synopsis [Performs phase abstraction by unrolling the circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVerbose ) +{ + Aig_Man_t * pFrames, * pAig = pTsi->pAig; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew; + Aig_Obj_t ** pObjMap; + unsigned * pState; + int i, f, Reg, Value; + + assert( Vec_IntSize(pTsi->vNonXRegs) > 0 ); + + // create mapping for the frames nodes + pObjMap = ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); + memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) ); + + // start the fraig package + pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); + pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + // map constant nodes + for ( f = 0; f < nFrames; f++ ) + Saig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); + // create PI nodes for the frames + for ( f = 0; f < nFrames; f++ ) + Aig_ManForEachPiSeq( pAig, pObj, i ) + Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) ); + // create the latches + Aig_ManForEachLoSeq( pAig, pObj, i ) + Saig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) ); + + // add timeframes + for ( f = 0; f < nFrames; f++ ) + { + // replace abstracted registers by constants + Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i ) + { + pObj = Saig_ManLo( pAig, Reg ); + pState = Vec_PtrEntry( pTsi->vStates, f ); + Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg ); + assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); + pObjNew = Value? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames); + Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); + } + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + { + pObjNew = Aig_And( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Saig_ObjChild1Frames(pObjMap,nFrames,pObj,f) ); + Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); + } + // set the latch inputs and copy them into the latch outputs of the next frame + Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i ) + { + pObjNew = Saig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f); + if ( f < nFrames - 1 ) + Saig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew ); + } + } + for ( f = 0; f < nFrames; f++ ) + { + Aig_ManForEachPoSeq( pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f) ); + Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); + } + } + pFrames->nRegs = pAig->nRegs; + pFrames->nTruePis = Aig_ManPiNum(pFrames) - Aig_ManRegNum(pFrames); + pFrames->nTruePos = Aig_ManPoNum(pFrames) - Aig_ManRegNum(pFrames); + Aig_ManForEachLiSeq( pAig, pObj, i ) + { + pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,nFrames-1) ); + Saig_ObjSetFrames( pObjMap, nFrames, pObj, nFrames-1, pObjNew ); + } +//Aig_ManPrintStats( pFrames ); + Aig_ManSeqCleanup( pFrames ); +//Aig_ManPrintStats( pFrames ); + Aig_ManPiCleanup( pFrames ); +//Aig_ManPrintStats( pFrames ); + free( pObjMap ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Performs automated phase abstraction.] + + Description [Takes the AIG manager and the array of initial states.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose ) +{ + Aig_Man_t * pNew = NULL; + Saig_Tsim_t * pTsi; + assert( Saig_ManRegNum(p) ); + assert( Saig_ManPiNum(p) ); + assert( Saig_ManPoNum(p) ); + // perform terminary simulation + pTsi = Saig_ManReachableTernary( p, vInits ); + if ( pTsi == NULL ) + return NULL; + // derive information + pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); + pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix; + pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords); + // print statistics + if ( fVerbose ) + { + printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n", + pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); + if ( pTsi->nNonXRegs < 100 ) + Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix ); + } + if ( fPrint ) + printf( "Print-out finished. Phase assignment is not performed.\n" ); + else if ( nFrames < 2 ) + printf( "The number of frames is less than 2. Phase assignment is not performed.\n" ); + else if ( pTsi->nCycle == 0 ) + printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" ); + else if ( pTsi->nCycle % nFrames != 0 ) + printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames ); + else if ( pTsi->nNonXRegs == 0 ) + printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" ); + else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) ) + printf( "There is no registers to abstract with %d frames.\n", nFrames ); + else + pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose ); + Saig_TsiStop( pTsi ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/saig/saig_.c b/src/aig/saig/saig_.c new file mode 100644 index 00000000..255639e6 --- /dev/null +++ b/src/aig/saig/saig_.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [saig_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saig_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |