| /**CFile**************************************************************** |
| |
| FileName [absOut.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Abstraction package.] |
| |
| Synopsis [Abstraction refinement outside of abstraction engines.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: absOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "abs.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derive a new counter-example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis ) |
| { |
| Abc_Cex_t * pCex; |
| int i, f, iPiNum; |
| assert( pCexAbs->iPo == 0 ); |
| // start the counter-example |
| pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 ); |
| pCex->iFrame = pCexAbs->iFrame; |
| pCex->iPo = pCexAbs->iPo; |
| // copy the bit data |
| for ( f = 0; f <= pCexAbs->iFrame; f++ ) |
| for ( i = 0; i < Vec_IntSize(vPis); i++ ) |
| { |
| if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) |
| { |
| iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) ); |
| Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum ); |
| } |
| } |
| // verify the counter example |
| if ( !Gia_ManVerifyCex( p, pCex, 0 ) ) |
| { |
| Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" ); |
| Abc_CexFree( pCex ); |
| pCex = NULL; |
| } |
| else |
| { |
| Abc_Print( 1, "Counter-example verification is successful.\n" ); |
| Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame ); |
| } |
| return pCex; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Refines gate-level abstraction using the counter-example.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ) |
| { |
| extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose ); |
| int fAddOneLayer = 1; |
| Abc_Cex_t * pCexNew = NULL; |
| Gia_Man_t * pAbs; |
| Aig_Man_t * pAig; |
| Abc_Cex_t * pCare; |
| Vec_Int_t * vPis, * vPPis; |
| int f, i, iObjId; |
| abctime clk = Abc_Clock(); |
| int nOnes = 0, Counter = 0; |
| if ( p->vGateClasses == NULL ) |
| { |
| Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" ); |
| return -1; |
| } |
| // derive abstraction |
| pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); |
| Gia_ManStop( pAbs ); |
| pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); |
| if ( Gia_ManPiNum(pAbs) != pCex->nPis ) |
| { |
| Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" ); |
| Gia_ManStop( pAbs ); |
| return -1; |
| } |
| if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) ) |
| { |
| Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" ); |
| // Gia_ManStop( pAbs ); |
| // return -1; |
| } |
| // else |
| // Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" ); |
| // get inputs |
| Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL ); |
| assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); |
| // add missing logic |
| if ( fAddOneLayer ) |
| { |
| Gia_Obj_t * pObj; |
| // check if this is a real counter-example |
| Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) ); |
| for ( f = 0; f <= pCex->iFrame; f++ ) |
| { |
| Gia_ManForEachPi( pAbs, pObj, i ) |
| { |
| if ( i >= Vec_IntSize(vPis) ) // PPIs |
| Gia_ObjTerSimSetX( pObj ); |
| else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) ) |
| Gia_ObjTerSimSet1( pObj ); |
| else |
| Gia_ObjTerSimSet0( pObj ); |
| } |
| Gia_ManForEachRo( pAbs, pObj, i ) |
| { |
| if ( f == 0 ) |
| Gia_ObjTerSimSet0( pObj ); |
| else |
| Gia_ObjTerSimRo( pAbs, pObj ); |
| } |
| Gia_ManForEachAnd( pAbs, pObj, i ) |
| Gia_ObjTerSimAnd( pObj ); |
| Gia_ManForEachCo( pAbs, pObj, i ) |
| Gia_ObjTerSimCo( pObj ); |
| } |
| pObj = Gia_ManPo( pAbs, 0 ); |
| if ( Gia_ObjTerSimGet1(pObj) ) |
| { |
| pCexNew = Gia_ManCexRemap( p, pCex, vPis ); |
| Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame ); |
| } |
| // else |
| // Abc_Print( 1, "CEX is not real.\n" ); |
| Gia_ManForEachObj( pAbs, pObj, i ) |
| Gia_ObjTerSimSetC( pObj ); |
| if ( pCexNew == NULL ) |
| { |
| // grow one layer |
| Vec_IntForEachEntry( vPPis, iObjId, i ) |
| { |
| assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 ); |
| Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 ); |
| } |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| } |
| } |
| else |
| { |
| // minimize the CEX |
| pAig = Gia_ManToAigSimple( pAbs ); |
| pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose ); |
| Aig_ManStop( pAig ); |
| if ( pCare == NULL ) |
| Abc_Print( 1, "Counter-example minimization has failed.\n" ); |
| // add new objects to the map |
| iObjId = -1; |
| for ( f = 0; f <= pCare->iFrame; f++ ) |
| for ( i = 0; i < pCare->nPis; i++ ) |
| if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) ) |
| { |
| nOnes++; |
| assert( i >= Vec_IntSize(vPis) ); |
| iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) ); |
| assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) ); |
| if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 ) |
| continue; |
| assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 ); |
| Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 ); |
| // Abc_Print( 1, "Adding object %d.\n", iObjId ); |
| // Gia_ObjPrint( p, Gia_ManObj(p, iObjId) ); |
| Counter++; |
| } |
| Abc_CexFree( pCare ); |
| if ( fVerbose ) |
| { |
| Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| // consider the case of SAT |
| if ( iObjId == -1 ) |
| { |
| pCexNew = Gia_ManCexRemap( p, pCex, vPis ); |
| Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame ); |
| } |
| } |
| Vec_IntFree( vPis ); |
| Vec_IntFree( vPPis ); |
| Gia_ManStop( pAbs ); |
| if ( pCexNew ) |
| { |
| ABC_FREE( p->pCexSeq ); |
| p->pCexSeq = pCexNew; |
| return 0; |
| } |
| // extract abstraction to include min-cut |
| if ( fMinCut ) |
| Nwk_ManDeriveMinCut( p, fVerbose ); |
| return -1; |
| } |
| |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Resimulates the counter-example and returns flop values.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Gia_ManGetStateAndCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame ) |
| { |
| Vec_Int_t * vInit = Vec_IntAlloc( Gia_ManRegNum(pAig) ); |
| Gia_Obj_t * pObj, * pObjRi, * pObjRo; |
| int RetValue, i, k, iBit = 0; |
| assert( iFrame >= 0 && iFrame <= p->iFrame ); |
| Gia_ManCleanMark0(pAig); |
| Gia_ManForEachRo( pAig, pObj, i ) |
| pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++); |
| for ( i = 0, iBit = p->nRegs; i <= p->iFrame; i++ ) |
| { |
| if ( i == iFrame ) |
| { |
| Gia_ManForEachRo( pAig, pObjRo, k ) |
| Vec_IntPush( vInit, pObjRo->fMark0 ); |
| } |
| Gia_ManForEachPi( pAig, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); |
| Gia_ManForEachAnd( pAig, pObj, k ) |
| pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & |
| (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); |
| Gia_ManForEachCo( pAig, pObj, k ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| if ( i == p->iFrame ) |
| break; |
| Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| assert( iBit == p->nBits ); |
| RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; |
| if ( RetValue != 1 ) |
| Vec_IntFreeP( &vInit ); |
| Gia_ManCleanMark0(pAig); |
| return vInit; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Verify counter-example starting in the given timeframe.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Gia_ManCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame ) |
| { |
| Gia_Obj_t * pObj, * pObjRi, * pObjRo; |
| int RetValue, i, k, iBit = 0; |
| assert( iFrame >= 0 && iFrame <= p->iFrame ); |
| Gia_ManCleanMark0(pAig); |
| Gia_ManForEachRo( pAig, pObj, i ) |
| pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++); |
| for ( i = iFrame, iBit += p->nRegs + Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ ) |
| { |
| Gia_ManForEachPi( pAig, pObj, k ) |
| pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); |
| Gia_ManForEachAnd( pAig, pObj, k ) |
| pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & |
| (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); |
| Gia_ManForEachCo( pAig, pObj, k ) |
| pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); |
| if ( i == p->iFrame ) |
| break; |
| Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k ) |
| pObjRo->fMark0 = pObjRi->fMark0; |
| } |
| assert( iBit == p->nBits ); |
| RetValue = Gia_ManPo(pAig, p->iPo)->fMark0; |
| Gia_ManCleanMark0(pAig); |
| if ( RetValue == 1 ) |
| printf( "Shortened CEX holds for the abstraction of the fast-forwarded model.\n" ); |
| else |
| printf( "Shortened CEX does not hold for the abstraction of the fast-forwarded model.\n" ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Gia_ManTransformFlops( Gia_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vInit ) |
| { |
| Vec_Bit_t * vInitNew; |
| Gia_Man_t * pNew; |
| Gia_Obj_t * pObj; |
| int i, iFlopId; |
| assert( Vec_IntSize(vInit) == Vec_IntSize(vFlops) ); |
| vInitNew = Vec_BitStart( Gia_ManRegNum(p) ); |
| Gia_ManForEachObjVec( vFlops, p, pObj, i ) |
| { |
| assert( Gia_ObjIsRo(p, pObj) ); |
| if ( Vec_IntEntry(vInit, i) == 0 ) |
| continue; |
| iFlopId = Gia_ObjCioId(pObj) - Gia_ManPiNum(p); |
| assert( iFlopId >= 0 && iFlopId < Gia_ManRegNum(p) ); |
| Vec_BitWriteEntry( vInitNew, iFlopId, 1 ); |
| } |
| pNew = Gia_ManDupFlip( p, Vec_BitArray(vInitNew) ); |
| Vec_BitFree( vInitNew ); |
| return pNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFrameExtra, int fVerbose ) |
| { |
| Gia_Man_t * pAbs, * pNew; |
| Vec_Int_t * vFlops, * vInit; |
| Vec_Int_t * vCopy; |
| // abctime clk = Abc_Clock(); |
| int RetValue; |
| ABC_FREE( p->pCexSeq ); |
| if ( p->vGateClasses == NULL ) |
| { |
| Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" ); |
| return -1; |
| } |
| vCopy = Vec_IntDup( p->vGateClasses ); |
| Abc_Print( 1, "Refining with %d-frame CEX, starting in frame %d, with %d extra frames.\n", pCex->iFrame, iFrameStart, iFrameExtra ); |
| // derive abstraction |
| pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); |
| Gia_ManStop( pAbs ); |
| pAbs = Gia_ManDupAbsGates( p, p->vGateClasses ); |
| if ( Gia_ManPiNum(pAbs) != pCex->nPis ) |
| { |
| Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" ); |
| Gia_ManStop( pAbs ); |
| Vec_IntFree( vCopy ); |
| return -1; |
| } |
| // get the state in frame iFrameStart |
| vInit = Gia_ManGetStateAndCheckCex( pAbs, pCex, iFrameStart ); |
| if ( vInit == NULL ) |
| { |
| Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" ); |
| Gia_ManStop( pAbs ); |
| Vec_IntFree( vCopy ); |
| return -1; |
| } |
| if ( fVerbose ) |
| Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" ); |
| // get inputs |
| Gia_ManGlaCollect( p, p->vGateClasses, NULL, NULL, &vFlops, NULL ); |
| // assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); |
| Gia_ManStop( pAbs ); |
| //Vec_IntPrint( vFlops ); |
| //Vec_IntPrint( vInit ); |
| // transform the manager to have new init state |
| pNew = Gia_ManTransformFlops( p, vFlops, vInit ); |
| Vec_IntFree( vFlops ); |
| Vec_IntFree( vInit ); |
| // verify abstraction |
| { |
| Gia_Man_t * pAbs = Gia_ManDupAbsGates( pNew, p->vGateClasses ); |
| Gia_ManCheckCex( pAbs, pCex, iFrameStart ); |
| Gia_ManStop( pAbs ); |
| } |
| // transfer abstraction |
| assert( pNew->vGateClasses == NULL ); |
| pNew->vGateClasses = Vec_IntDup( p->vGateClasses ); |
| // perform abstraction for the new AIG |
| { |
| Abs_Par_t Pars, * pPars = &Pars; |
| Abs_ParSetDefaults( pPars ); |
| pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra; |
| pPars->fVerbose = fVerbose; |
| RetValue = Gia_ManPerformGla( pNew, pPars ); |
| if ( RetValue == 0 ) // spurious SAT |
| { |
| Vec_IntFreeP( &pNew->vGateClasses ); |
| pNew->vGateClasses = Vec_IntDup( vCopy ); |
| } |
| } |
| // move the abstraction map |
| Vec_IntFreeP( &p->vGateClasses ); |
| p->vGateClasses = pNew->vGateClasses; |
| pNew->vGateClasses = NULL; |
| // cleanup |
| Gia_ManStop( pNew ); |
| Vec_IntFree( vCopy ); |
| return -1; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
