| /**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" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| /* |
| 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 (Aig_ManRandom(0) & 1) ? SAIG_XVS1 : SAIG_XVS0; |
| } |
| static inline int Saig_XsimRand3() |
| { |
| int RetValue; |
| do { |
| RetValue = Aig_ManRandom(0) & 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 *)ABC_ALLOC( char, sizeof(Saig_Tsim_t) ); |
| memset( p, 0, sizeof(Saig_Tsim_t) ); |
| p->pAig = pAig; |
| p->nWords = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) ); |
| p->vStates = Vec_PtrAlloc( 1000 ); |
| p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 ); |
| p->nBins = Abc_PrimeCudd(TSIM_MAX_ROUNDS/2); |
| p->pBins = ABC_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 ); |
| ABC_FREE( p->pBins ); |
| ABC_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 nPref ) |
| { |
| 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_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, nPref ) |
| { |
| Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_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 [Computes flops that are stuck-at constant.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref ) |
| { |
| Vec_Int_t * vCounters; |
| unsigned * pState; |
| int ValueThis = -1, ValuePrev = -1, StepPrev = -1; |
| int i, k, nRegs = p->pAig->nRegs; |
| vCounters = Vec_IntStart( nPref ); |
| for ( i = 0; i < nRegs; i++ ) |
| { |
| Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k ) |
| { |
| ValueThis = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); |
| //printf( "%s", (ValueThis == 1)? "0" : ((ValueThis == 2)? "1" : "x") ); |
| assert( ValueThis != 0 ); |
| if ( ValuePrev != ValueThis ) |
| { |
| ValuePrev = ValueThis; |
| StepPrev = k; |
| } |
| } |
| //printf( "\n" ); |
| if ( ValueThis == SAIG_XVSX ) |
| continue; |
| if ( StepPrev >= nPref ) |
| continue; |
| Vec_IntAddToEntry( vCounters, StepPrev, 1 ); |
| } |
| Vec_IntForEachEntry( vCounters, ValueThis, i ) |
| { |
| if ( ValueThis == 0 ) |
| continue; |
| // printf( "%3d : %3d\n", i, ValueThis ); |
| } |
| return vCounters; |
| } |
| |
| /**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, int nLoop ) |
| { |
| unsigned * pState; |
| int nRegs = p->pAig->nRegs; |
| int Value, i, k, Counter = 0; |
| printf( "Ternary traces for each flop:\n" ); |
| printf( " : " ); |
| for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ ) |
| printf( "%d", i%10 ); |
| printf( " " ); |
| for ( i = 0; i < nLoop; i++ ) |
| printf( "%d", i%10 ); |
| printf( "\n" ); |
| for ( i = 0; i < nRegs; i++ ) |
| { |
| /* |
| Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k ) |
| { |
| Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); |
| if ( Value == SAIG_XVSX ) |
| break; |
| } |
| if ( k == Vec_PtrSize(p->vStates) ) |
| Counter++; |
| else |
| continue; |
| */ |
| |
| // print trace |
| // printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id ); |
| printf( "%5d : ", Counter++ ); |
| Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) |
| { |
| Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_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( unsigned *, 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 = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_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 = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_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( unsigned *, 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, int fVerbose ) |
| { |
| 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 ) |
| Abc_InfoSetBit( pState, 2 * i ); |
| if ( Value & 2 ) |
| Abc_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 ) ) |
| { |
| if ( fVerbose ) |
| printf( "Ternary simulation converged after %d iterations.\n", f ); |
| 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 [Analize initial value of the selected register.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg ) |
| { |
| Aig_Obj_t * pObj, * pReg, * pCtrl, * pAnd; |
| int i; |
| pReg = Saig_ManLo( p, Reg ); |
| pCtrl = Saig_ManLo( p, Saig_ManRegNum(p)-1 ); |
| assert( pReg->Id < pCtrl->Id ); |
| // find a node pointing to both |
| pAnd = NULL; |
| Aig_ManForEachNode( p, pObj, i ) |
| { |
| if ( Aig_ObjFanin0(pObj) == pReg && Aig_ObjFanin1(pObj) == pCtrl ) |
| { |
| pAnd = pObj; |
| break; |
| } |
| } |
| if ( pAnd == NULL ) |
| { |
| printf( "Register is not found.\n" ); |
| return; |
| } |
| printf( "Clock-like register: \n" ); |
| Aig_ObjPrint( p, pReg ); |
| printf( "\n" ); |
| printf( "Control register: \n" ); |
| Aig_ObjPrint( p, pCtrl ); |
| printf( "\n" ); |
| printf( "Their fanout: \n" ); |
| Aig_ObjPrint( p, pAnd ); |
| printf( "\n" ); |
| |
| // find the fanouts of pAnd |
| printf( "Fanouts of the fanout: \n" ); |
| Aig_ManForEachObj( p, pObj, i ) |
| if ( Aig_ObjFanin0(pObj) == pAnd || Aig_ObjFanin1(pObj) == pAnd ) |
| { |
| Aig_ObjPrint( p, pObj ); |
| printf( "\n" ); |
| } |
| printf( "\n" ); |
| } |
| |
| /**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[257] = {0}; |
| 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 = (unsigned *)Vec_PtrEntry( pTsi->vStates, k ); |
| else |
| pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle ); |
| Value = (Abc_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Abc_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" ); |
| |
| if ( fVerbose ) |
| Saig_ManAnalizeControl( pTsi->pAig, Reg ); |
| } |
| } |
| 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 = ABC_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 = Abc_UtilStrsav( pAig->pName ); |
| pFrames->pSpec = Abc_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_ObjCreateCi(pFrames) ); |
| // create the latches |
| Aig_ManForEachLoSeq( pAig, pObj, i ) |
| Saig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(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 = (unsigned *)Vec_PtrEntry( pTsi->vStates, f ); |
| Value = (Abc_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * Reg ); |
| assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); |
| pObjNew = (Value == SAIG_XVS1)? 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_ObjCreateCo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f) ); |
| Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); |
| } |
| } |
| pFrames->nRegs = pAig->nRegs; |
| pFrames->nTruePis = Aig_ManCiNum(pFrames) - Aig_ManRegNum(pFrames); |
| pFrames->nTruePos = Aig_ManCoNum(pFrames) - Aig_ManRegNum(pFrames); |
| Aig_ManForEachLiSeq( pAig, pObj, i ) |
| { |
| pObjNew = Aig_ObjCreateCo( 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_ManCiCleanup( pFrames ); |
| //Aig_ManPrintStats( pFrames ); |
| ABC_FREE( pObjMap ); |
| return pFrames; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs automated phase abstraction.] |
| |
| Description [Takes the AIG manager and the array of initial states.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits ) |
| { |
| Saig_Tsim_t * pTsi; |
| int nFrames, nPrefix; |
| assert( Saig_ManRegNum(p) ); |
| assert( Saig_ManPiNum(p) ); |
| assert( Saig_ManPoNum(p) ); |
| // perform terminary simulation |
| pTsi = Saig_ManReachableTernary( p, vInits, 0 ); |
| if ( pTsi == NULL ) |
| return 1; |
| // derive information |
| nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); |
| nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix; |
| Saig_TsiStop( pTsi ); |
| // potentially, may need to reduce nFrames if nPrefix is less than nFrames |
| return nFrames; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs automated phase abstraction.] |
| |
| Description [Takes the AIG manager and the array of initial states.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans ) |
| { |
| Saig_Tsim_t * pTsi; |
| int nFrames, nPrefix, nNonXRegs; |
| assert( Saig_ManRegNum(p) ); |
| assert( Saig_ManPiNum(p) ); |
| assert( Saig_ManPoNum(p) ); |
| // perform terminary simulation |
| pTsi = Saig_ManReachableTernary( p, NULL, 0 ); |
| if ( pTsi == NULL ) |
| return 0; |
| // derive information |
| nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); |
| nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix; |
| nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, nPrefix ); |
| |
| if ( pvTrans ) |
| *pvTrans = Saig_TsiComputeTransient( pTsi, nPrefix ); |
| |
| // print statistics |
| if ( fVerbose ) |
| printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs ); |
| if ( fVeryVerbose ) |
| Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames ); |
| Saig_TsiStop( pTsi ); |
| // potentially, may need to reduce nFrames if nPrefix is less than nFrames |
| return nPrefix; |
| } |
| |
| /**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 nPref, 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, fVerbose ); |
| if ( pTsi == NULL ) |
| return NULL; |
| // derive information |
| pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); |
| pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix; |
| pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, Abc_MinInt(pTsi->nPrefix,nPref)); |
| // print statistics |
| if ( fVerbose ) |
| { |
| printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", |
| pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); |
| if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 ) |
| Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle ); |
| } |
| 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 ( nFrames > 256 ) |
| printf( "The number of frames is more than 256. Phase assignment is not performed.\n" ); |
| else if ( pTsi->nCycle == 1 ) |
| 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; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Performs automated phase abstraction.] |
| |
| Description [Takes the AIG manager and the array of initial states.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) |
| { |
| Aig_Man_t * pNew = NULL; |
| Saig_Tsim_t * pTsi; |
| int fPrint = 0; |
| int nFrames; |
| assert( Saig_ManRegNum(p) ); |
| assert( Saig_ManPiNum(p) ); |
| assert( Saig_ManPoNum(p) ); |
| // perform terminary simulation |
| pTsi = Saig_ManReachableTernary( p, NULL, fVerbose ); |
| if ( pTsi == NULL ) |
| return NULL; |
| // derive information |
| pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); |
| pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix; |
| pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, 0); |
| // print statistics |
| if ( fVerbose ) |
| { |
| printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", |
| pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs ); |
| if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 ) |
| Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle ); |
| } |
| nFrames = pTsi->nCycle; |
| 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 ( nFrames > 256 ) |
| { |
| // printf( "The number of frames is more than 256. Phase assignment is not performed.\n" ); |
| } |
| else if ( pTsi->nCycle == 1 ) |
| { |
| // 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, 0, fVerbose ) ) |
| { |
| // printf( "There is no registers to abstract with %d frames.\n", nFrames ); |
| } |
| else |
| pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose ); |
| Saig_TsiStop( pTsi ); |
| if ( pNew == NULL ) |
| pNew = Aig_ManDupSimple( p ); |
| if ( Aig_ManCiNum(pNew) == Aig_ManRegNum(pNew) ) |
| { |
| Aig_ManStop( pNew); |
| pNew = Aig_ManDupSimple( p ); |
| } |
| return pNew; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives CEX for the original AIG from CEX of the unrolled AIG.] |
| |
| Description [The number of PIs of the given CEX should divide by the number |
| of PIs of the original AIG without a remainder.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex ) |
| { |
| Abc_Cex_t * pNew; |
| int i, k, iFrame, nFrames; |
| // make sure the PI count of the AIG is a multiple of the PI count of the CEX |
| // if this is not true, the CEX is not derived as the result of unrolling of pAig |
| // or the unrolled CEX went through transformations that change the PI count |
| if ( pCex->nPis % Saig_ManPiNum(p) != 0 ) |
| { |
| printf( "The PI count in the AIG and in the CEX do not match.\n" ); |
| return NULL; |
| } |
| // get the number of unrolled frames |
| nFrames = pCex->nPis / Saig_ManPiNum(p); |
| // get the frame where it fails |
| iFrame = pCex->iFrame * nFrames + pCex->iPo / Saig_ManPoNum(p); |
| // start a new CEX (assigns: p->nRegs, p->nPis, p->nBits) |
| pNew = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), iFrame+1 ); |
| assert( pNew->nBits == pNew->nPis * (iFrame + 1) + pNew->nRegs ); |
| // now assign the failed frame and the failed PO (p->iFrame and p->iPo) |
| pNew->iFrame = iFrame; |
| pNew->iPo = pCex->iPo % Saig_ManPoNum(p); |
| // copy the bit data |
| for ( i = pCex->nRegs, k = pNew->nRegs; k < pNew->nBits; k++, i++ ) |
| if ( Abc_InfoHasBit( pCex->pData, i ) ) |
| Abc_InfoSetBit( pNew->pData, k ); |
| assert( i <= pCex->nBits ); |
| return pNew; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
