/**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