| /**CFile**************************************************************** |
| |
| FileName [bmcInse.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT-based bounded model checking.] |
| |
| Synopsis [] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "bmc.h" |
| #include "sat/cnf/cnf.h" |
| #include "sat/bsat/satStore.h" |
| #include "aig/gia/giaAig.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static inline void Gia_ParTestAlloc( Gia_Man_t * p, int nWords ) { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, 2*nWords*Gia_ManObjNum(p)); p->iData = nWords; } |
| static inline void Gia_ParTestFree( Gia_Man_t * p ) { ABC_FREE( p->pData ); p->iData = 0; } |
| static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (word *)p->pData + Id*(p->iData << 1); } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManInseInit( Gia_Man_t * p, Vec_Int_t * vInit ) |
| { |
| Gia_Obj_t * pObj; |
| word * pData1, * pData0; |
| int i, k; |
| Gia_ManForEachRi( p, pObj, k ) |
| { |
| pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) ); |
| pData1 = pData0 + p->iData; |
| if ( Vec_IntEntry(vInit, k) == 0 ) // 0 |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = ~(word)0, pData1[i] = 0; |
| else if ( Vec_IntEntry(vInit, k) == 1 ) // 1 |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = 0, pData1[i] = ~(word)0; |
| else // if ( Vec_IntEntry(vInit, k) > 1 ) // X |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = pData1[i] = 0; |
| } |
| } |
| void Gia_ManInseSimulateObj( Gia_Man_t * p, int Id ) |
| { |
| Gia_Obj_t * pObj = Gia_ManObj( p, Id ); |
| word * pData0, * pDataA0, * pDataB0; |
| word * pData1, * pDataA1, * pDataB1; |
| int i; |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| pData0 = Gia_ParTestObj( p, Id ); |
| pData1 = pData0 + p->iData; |
| if ( Gia_ObjFaninC0(pObj) ) |
| { |
| pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) ); |
| pDataA0 = pDataA1 + p->iData; |
| if ( Gia_ObjFaninC1(pObj) ) |
| { |
| pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) ); |
| pDataB0 = pDataB1 + p->iData; |
| } |
| else |
| { |
| pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) ); |
| pDataB1 = pDataB0 + p->iData; |
| } |
| } |
| else |
| { |
| pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) ); |
| pDataA1 = pDataA0 + p->iData; |
| if ( Gia_ObjFaninC1(pObj) ) |
| { |
| pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) ); |
| pDataB0 = pDataB1 + p->iData; |
| } |
| else |
| { |
| pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) ); |
| pDataB1 = pDataB0 + p->iData; |
| } |
| } |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = pDataA0[i] | pDataB0[i], pData1[i] = pDataA1[i] & pDataB1[i]; |
| } |
| else if ( Gia_ObjIsCo(pObj) ) |
| { |
| pData0 = Gia_ParTestObj( p, Id ); |
| pData1 = pData0 + p->iData; |
| if ( Gia_ObjFaninC0(pObj) ) |
| { |
| pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) ); |
| pDataA0 = pDataA1 + p->iData; |
| } |
| else |
| { |
| pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) ); |
| pDataA1 = pDataA0 + p->iData; |
| } |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = pDataA0[i], pData1[i] = pDataA1[i]; |
| } |
| else if ( Gia_ObjIsCi(pObj) ) |
| { |
| if ( Gia_ObjIsPi(p, pObj) ) |
| { |
| pData0 = Gia_ParTestObj( p, Id ); |
| pData1 = pData0 + p->iData; |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = Gia_ManRandomW(0), pData1[i] = ~pData0[i]; |
| } |
| else |
| { |
| int Id2 = Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)); |
| pData0 = Gia_ParTestObj( p, Id ); |
| pData1 = pData0 + p->iData; |
| pDataA0 = Gia_ParTestObj( p, Id2 ); |
| pDataA1 = pDataA0 + p->iData; |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = pDataA0[i], pData1[i] = pDataA1[i]; |
| } |
| } |
| else if ( Gia_ObjIsConst0(pObj) ) |
| { |
| pData0 = Gia_ParTestObj( p, Id ); |
| pData1 = pData0 + p->iData; |
| for ( i = 0; i < p->iData; i++ ) |
| pData0[i] = ~(word)0, pData1[i] = 0; |
| } |
| else assert( 0 ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManInseHighestScore( Gia_Man_t * p, int * pCost ) |
| { |
| Gia_Obj_t * pObj; |
| word * pData0, * pData1; |
| int * pCounts, CountBest; |
| int i, k, b, nPats, iPat; |
| nPats = 64 * p->iData; |
| pCounts = ABC_CALLOC( int, nPats ); |
| Gia_ManForEachRi( p, pObj, k ) |
| { |
| pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) ); |
| pData1 = pData0 + p->iData; |
| for ( i = 0; i < p->iData; i++ ) |
| for ( b = 0; b < 64; b++ ) |
| pCounts[64*i+b] += (((pData0[i] >> b) & 1) || ((pData1[i] >> b) & 1)); // binary |
| } |
| iPat = 0; |
| CountBest = pCounts[0]; |
| for ( k = 1; k < nPats; k++ ) |
| if ( CountBest < pCounts[k] ) |
| CountBest = pCounts[k], iPat = k; |
| *pCost = Gia_ManRegNum(p) - CountBest; // ternary |
| ABC_FREE( pCounts ); |
| return iPat; |
| } |
| void Gia_ManInseFindStarting( Gia_Man_t * p, int iPat, Vec_Int_t * vInit, Vec_Int_t * vInputs ) |
| { |
| Gia_Obj_t * pObj; |
| word * pData0, * pData1; |
| int i, k; |
| Vec_IntClear( vInit ); |
| Gia_ManForEachRi( p, pObj, k ) |
| { |
| pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) ); |
| pData1 = pData0 + p->iData; |
| for ( i = 0; i < p->iData; i++ ) |
| assert( (pData0[i] & pData1[i]) == 0 ); |
| if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) ) |
| Vec_IntPush( vInit, 0 ); |
| else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) ) |
| Vec_IntPush( vInit, 1 ); |
| else |
| Vec_IntPush( vInit, 2 ); |
| } |
| Gia_ManForEachPi( p, pObj, k ) |
| { |
| pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) ); |
| pData1 = pData0 + p->iData; |
| for ( i = 0; i < p->iData; i++ ) |
| assert( (pData0[i] & pData1[i]) == 0 ); |
| if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) ) |
| Vec_IntPush( vInputs, 0 ); |
| else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) ) |
| Vec_IntPush( vInputs, 1 ); |
| else |
| Vec_IntPush( vInputs, 2 ); |
| } |
| } |
| Vec_Int_t * Gia_ManInseSimulate( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInputs, Vec_Int_t * vInit ) |
| { |
| Vec_Int_t * vRes; |
| Gia_Obj_t * pObj, * pObjRo, * pObjRi; |
| int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p); |
| int i, f, iBit = 0; |
| assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 ); |
| assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) ); |
| assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) ); |
| Gia_ManConst0(p)->fMark0 = 0; |
| Gia_ManForEachRi( p, pObj, i ) |
| pObj->fMark0 = Vec_IntEntry(vInit0, i); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Gia_ManForEachPi( p, pObj, i ) |
| pObj->fMark0 = Vec_IntEntry(vInputs, iBit++); |
| Gia_ManForEachAnd( p, pObj, i ) |
| pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & |
| (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); |
| Gia_ManForEachRi( p, pObj, i ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| assert( iBit == Vec_IntSize(vInputs) ); |
| vRes = Vec_IntAlloc( Gia_ManRegNum(p) ); |
| Gia_ManForEachRo( p, pObj, i ) |
| assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 ); |
| Gia_ManForEachRo( p, pObj, i ) |
| Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) ); |
| Gia_ManForEachObj( p, pObj, i ) |
| pObj->fMark0 = 0; |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_ManInsePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose ) |
| { |
| Vec_Int_t * vRes, * vInit, * vInputs; |
| Gia_Obj_t * pObj; |
| int i, f, iPat, Cost, Cost0; |
| abctime clk, clkTotal = Abc_Clock(); |
| Gia_ManRandomW( 1 ); |
| if ( fVerbose ) |
| printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " ); |
| vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 ); |
| vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames ); |
| Gia_ParTestAlloc( p, nWords ); |
| Gia_ManInseInit( p, vInit ); |
| Cost0 = 0; |
| Vec_IntForEachEntry( vInit, iPat, i ) |
| Cost0 += ((iPat >> 1) & 1); |
| if ( fVerbose ) |
| printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Cost0, Cost0 ); |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| clk = Abc_Clock(); |
| Gia_ManForEachObj( p, pObj, i ) |
| Gia_ManInseSimulateObj( p, i ); |
| iPat = Gia_ManInseHighestScore( p, &Cost ); |
| Gia_ManInseFindStarting( p, iPat, vInit, vInputs ); |
| Gia_ManInseInit( p, vInit ); |
| if ( fVerbose ) |
| printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 ); |
| if ( fVerbose ) |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| Gia_ParTestFree( p ); |
| vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit ); |
| Vec_IntFreeP( &vInit ); |
| Vec_IntFreeP( &vInputs ); |
| printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) ); |
| Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) |
| { |
| Vec_Int_t * vRes, * vInit; |
| vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 ); |
| vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose ); |
| if ( vInit != vInit0 ) |
| Vec_IntFree( vInit ); |
| return vRes; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
