| /**CFile**************************************************************** |
| |
| FileName [saigSimSeq.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Sequential AIG package.] |
| |
| Synopsis [Fast sequential AIG simulator.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: saigSimSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "saig.h" |
| #include "proof/ssw/ssw.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // combinational simulation manager |
| typedef struct Raig_Man_t_ Raig_Man_t; |
| struct Raig_Man_t_ |
| { |
| // parameters |
| Aig_Man_t * pAig; // the AIG to be used for simulation |
| int nWords; // the number of words to simulate |
| // AIG representation |
| int nPis; // the number of primary inputs |
| int nPos; // the number of primary outputs |
| int nCis; // the number of combinational inputs |
| int nCos; // the number of combinational outputs |
| int nNodes; // the number of internal nodes |
| int nObjs; // nCis + nNodes + nCos + 2 |
| int * pFans0; // fanin0 for all objects |
| int * pFans1; // fanin1 for all objects |
| Vec_Int_t * vCis2Ids; // mapping of CIs into their PI ids |
| Vec_Int_t * vLos; // register outputs |
| Vec_Int_t * vLis; // register inputs |
| // simulation info |
| int * pRefs; // reference counter for each node |
| unsigned * pSims; // simlulation information for each node |
| // recycable memory |
| unsigned * pMems; // allocated simulaton memory |
| int nWordsAlloc; // the number of allocated entries |
| int nMems; // the number of used entries |
| int nMemsMax; // the max number of used entries |
| int MemFree; // next free entry |
| }; |
| |
| static inline int Raig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } |
| static inline int Raig_Lit2Var( int Lit ) { return Lit >> 1; } |
| static inline int Raig_LitIsCompl( int Lit ) { return Lit & 1; } |
| static inline int Raig_LitNot( int Lit ) { return Lit ^ 1; } |
| static inline int Raig_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } |
| static inline int Raig_LitRegular( int Lit ) { return Lit & ~01; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Find the PO corresponding to the PO driver.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Raig_ManFindPo( Aig_Man_t * pAig, int iNode ) |
| { |
| Aig_Obj_t * pObj; |
| int i; |
| Saig_ManForEachPo( pAig, pObj, i ) |
| if ( pObj->iData == iNode ) |
| return i; |
| return -1; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates fast simulation manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj ) |
| { |
| int iFan0, iFan1; |
| assert( !Aig_IsComplement(pObj) ); |
| if ( pObj->iData ) |
| return pObj->iData; |
| assert( !Aig_ObjIsConst1(pObj) ); |
| if ( Aig_ObjIsNode(pObj) ) |
| { |
| iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) ); |
| iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj); |
| iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) ); |
| iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj); |
| } |
| else if ( Aig_ObjIsCo(pObj) ) |
| { |
| iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) ); |
| iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj); |
| iFan1 = 0; |
| } |
| else |
| { |
| iFan0 = iFan1 = 0; |
| Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) ); |
| } |
| p->pFans0[p->nObjs] = iFan0; |
| p->pFans1[p->nObjs] = iFan1; |
| p->pRefs[p->nObjs] = Aig_ObjRefs(pObj); |
| return pObj->iData = p->nObjs++; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates fast simulation manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig ) |
| { |
| Raig_Man_t * p; |
| Aig_Obj_t * pObj; |
| int i, nObjs; |
| Aig_ManCleanData( pAig ); |
| p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 ); |
| memset( p, 0, sizeof(Raig_Man_t) ); |
| p->pAig = pAig; |
| p->nPis = Saig_ManPiNum(pAig); |
| p->nPos = Saig_ManPoNum(pAig); |
| p->nCis = Aig_ManCiNum(pAig); |
| p->nCos = Aig_ManCoNum(pAig); |
| p->nNodes = Aig_ManNodeNum(pAig); |
| nObjs = p->nCis + p->nCos + p->nNodes + 2; |
| p->pFans0 = ABC_ALLOC( int, nObjs ); |
| p->pFans1 = ABC_ALLOC( int, nObjs ); |
| p->pRefs = ABC_ALLOC( int, nObjs ); |
| p->pSims = ABC_CALLOC( unsigned, nObjs ); |
| p->vCis2Ids = Vec_IntAlloc( Aig_ManCiNum(pAig) ); |
| // add objects (0=unused; 1=const1) |
| p->nObjs = 2; |
| pObj = Aig_ManConst1( pAig ); |
| pObj->iData = 1; |
| Aig_ManForEachCi( pAig, pObj, i ) |
| if ( Aig_ObjRefs(pObj) == 0 ) |
| Raig_ManCreate_rec( p, pObj ); |
| Aig_ManForEachCo( pAig, pObj, i ) |
| Raig_ManCreate_rec( p, pObj ); |
| assert( Vec_IntSize(p->vCis2Ids) == Aig_ManCiNum(pAig) ); |
| assert( p->nObjs == nObjs ); |
| // collect flop outputs |
| p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) ); |
| Saig_ManForEachLo( pAig, pObj, i ) |
| Vec_IntPush( p->vLos, pObj->iData ); |
| // collect flop inputs |
| p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) ); |
| Saig_ManForEachLi( pAig, pObj, i ) |
| { |
| Vec_IntPush( p->vLis, pObj->iData ); |
| assert( p->pRefs[ pObj->iData ] == 0 ); |
| p->pRefs[ pObj->iData ]++; |
| } |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates fast simulation manager.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Raig_ManDelete( Raig_Man_t * p ) |
| { |
| Vec_IntFree( p->vCis2Ids ); |
| Vec_IntFree( p->vLos ); |
| Vec_IntFree( p->vLis ); |
| ABC_FREE( p->pFans0 ); |
| ABC_FREE( p->pFans1 ); |
| ABC_FREE( p->pRefs ); |
| ABC_FREE( p->pSims ); |
| ABC_FREE( p->pMems ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [References simulation info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned * Raig_ManSimRef( Raig_Man_t * p, int i ) |
| { |
| unsigned * pSim; |
| assert( i > 1 ); |
| assert( p->pSims[i] == 0 ); |
| if ( p->MemFree == 0 ) |
| { |
| unsigned * pPlace, Ent; |
| if ( p->nWordsAlloc == 0 ) |
| { |
| assert( p->pMems == NULL ); |
| p->nWordsAlloc = (1<<17); // -> 1Mb |
| p->nMems = 1; |
| } |
| p->nWordsAlloc *= 2; |
| p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc ); |
| memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) ); |
| pPlace = (unsigned *)&p->MemFree; |
| for ( Ent = p->nMems * (p->nWords + 1); |
| Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc; |
| Ent += p->nWords + 1 ) |
| { |
| *pPlace = Ent; |
| pPlace = p->pMems + Ent; |
| } |
| *pPlace = 0; |
| } |
| p->pSims[i] = p->MemFree; |
| pSim = p->pMems + p->MemFree; |
| p->MemFree = pSim[0]; |
| pSim[0] = p->pRefs[i]; |
| p->nMems++; |
| if ( p->nMemsMax < p->nMems ) |
| p->nMemsMax = p->nMems; |
| return pSim; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Dereference simulaton info.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| unsigned * Raig_ManSimDeref( Raig_Man_t * p, int i ) |
| { |
| unsigned * pSim; |
| assert( i ); |
| if ( i == 1 ) // const 1 |
| return p->pMems; |
| assert( p->pSims[i] > 0 ); |
| pSim = p->pMems + p->pSims[i]; |
| if ( --pSim[0] == 0 ) |
| { |
| pSim[0] = p->MemFree; |
| p->MemFree = p->pSims[i]; |
| p->pSims[i] = 0; |
| p->nMems--; |
| } |
| return pSim; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Simulates one round.] |
| |
| Description [Returns the number of PO entry if failed; 0 otherwise.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Raig_ManSimulateRound( Raig_Man_t * p, int fMiter, int fFirst, int * piPat ) |
| { |
| unsigned * pRes0, * pRes1, * pRes; |
| int i, w, nCis, nCos, iFan0, iFan1, iPioNum; |
| // nove the values to the register outputs |
| Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i ) |
| { |
| if ( iPioNum < p->nPis ) |
| continue; |
| pRes = Raig_ManSimRef( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) ); |
| if ( fFirst ) |
| memset( pRes + 1, 0, sizeof(unsigned) * p->nWords ); |
| else |
| { |
| pRes0 = Raig_ManSimDeref( p, Vec_IntEntry(p->vLis, iPioNum-p->nPis) ); |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = pRes0[w]; |
| } |
| // handle unused PIs |
| if ( pRes[0] == 0 ) |
| { |
| pRes[0] = 1; |
| Raig_ManSimDeref( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) ); |
| } |
| } |
| // simulate the logic |
| nCis = nCos = 0; |
| for ( i = 2; i < p->nObjs; i++ ) |
| { |
| if ( p->pFans0[i] == 0 ) // ci always has zero first fanin |
| { |
| iPioNum = Vec_IntEntry( p->vCis2Ids, nCis ); |
| if ( iPioNum < p->nPis ) |
| { |
| pRes = Raig_ManSimRef( p, i ); |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = Aig_ManRandom( 0 ); |
| // handle unused PIs |
| if ( pRes[0] == 0 ) |
| { |
| pRes[0] = 1; |
| Raig_ManSimDeref( p, i ); |
| } |
| } |
| else |
| assert( Vec_IntEntry(p->vLos, iPioNum-p->nPis) == i ); |
| nCis++; |
| continue; |
| } |
| if ( p->pFans1[i] == 0 ) // co always has non-zero 1st fanin and zero 2nd fanin |
| { |
| pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) ); |
| if ( nCos < p->nPos && fMiter ) |
| { |
| unsigned Const = Raig_LitIsCompl(p->pFans0[i])? ~0 : 0; |
| for ( w = 1; w <= p->nWords; w++ ) |
| if ( pRes0[w] != Const ) |
| { |
| *piPat = 32*(w-1) + Aig_WordFindFirstBit( pRes0[w] ^ Const ); |
| return i; |
| } |
| } |
| else |
| { |
| pRes = Raig_ManSimRef( p, i ); |
| assert( pRes[0] == 1 ); |
| if ( Raig_LitIsCompl(p->pFans0[i]) ) |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = ~pRes0[w]; |
| else |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = pRes0[w]; |
| } |
| nCos++; |
| continue; |
| } |
| pRes = Raig_ManSimRef( p, i ); |
| assert( pRes[0] > 0 ); |
| iFan0 = p->pFans0[i]; |
| iFan1 = p->pFans1[i]; |
| pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) ); |
| pRes1 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans1[i]) ); |
| if ( Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) ) |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = ~(pRes0[w] | pRes1[w]); |
| else if ( Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) ) |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = ~pRes0[w] & pRes1[w]; |
| else if ( !Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) ) |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = pRes0[w] & ~pRes1[w]; |
| else if ( !Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) ) |
| for ( w = 1; w <= p->nWords; w++ ) |
| pRes[w] = pRes0[w] & pRes1[w]; |
| } |
| assert( nCis == p->nCis ); |
| assert( nCos == p->nCos ); |
| assert( p->nMems == 1 + Vec_IntSize(p->vLis) ); |
| return 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the counter-example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids ) |
| { |
| Abc_Cex_t * p; |
| unsigned * pData; |
| int f, i, w, iPioId, Counter; |
| p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 ); |
| p->iFrame = iFrame; |
| p->iPo = iOut; |
| // fill in the binary data |
| Aig_ManRandom( 1 ); |
| Counter = p->nRegs; |
| pData = ABC_ALLOC( unsigned, nWords ); |
| for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) |
| for ( i = 0; i < Aig_ManCiNum(pAig); i++ ) |
| { |
| iPioId = Vec_IntEntry( vCis2Ids, i ); |
| if ( iPioId >= p->nPis ) |
| continue; |
| for ( w = 0; w < nWords; w++ ) |
| pData[w] = Aig_ManRandom( 0 ); |
| if ( Abc_InfoHasBit( pData, iPat ) ) |
| Abc_InfoSetBit( p->pData, Counter + iPioId ); |
| } |
| ABC_FREE( pData ); |
| return p; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns 1 if the bug is detected, 0 otherwise.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose ) |
| { |
| Raig_Man_t * p; |
| Sec_MtrStatus_t Status; |
| int i, iPat, RetValue = 0; |
| abctime clk, clkTotal = Abc_Clock(); |
| assert( Aig_ManRegNum(pAig) > 0 ); |
| Status = Sec_MiterStatus( pAig ); |
| if ( Status.nSat > 0 ) |
| { |
| printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut ); |
| return 1; |
| } |
| if ( Status.nUndec == 0 ) |
| { |
| printf( "Miter is trivially unsatisfiable.\n" ); |
| return 0; |
| } |
| Aig_ManRandom( 1 ); |
| p = Raig_ManCreate( pAig ); |
| p->nWords = nWords; |
| // iterate through objects |
| for ( i = 0; i < nIters; i++ ) |
| { |
| clk = Abc_Clock(); |
| RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat ); |
| if ( fVerbose ) |
| { |
| printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit ); |
| printf("Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC); |
| } |
| if ( RetValue > 0 ) |
| { |
| int iOut = Raig_ManFindPo(p->pAig, RetValue); |
| assert( pAig->pSeqModel == NULL ); |
| pAig->pSeqModel = Raig_ManGenerateCounter( pAig, i, iOut, nWords, iPat, p->vCis2Ids ); |
| if ( fVerbose ) |
| printf( "Miter is satisfiable after simulation (output %d).\n", iOut ); |
| break; |
| } |
| if ( (Abc_Clock() - clk)/CLOCKS_PER_SEC >= TimeLimit ) |
| { |
| printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit ); |
| break; |
| } |
| } |
| if ( fVerbose ) |
| { |
| printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ", |
| p->nMemsMax, |
| 1.0*(p->nObjs * 16)/(1<<20), |
| 1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) ); |
| ABC_PRT( "Total time", Abc_Clock() - clkTotal ); |
| } |
| Raig_ManDelete( p ); |
| return RetValue > 0; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
