diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-15 23:27:46 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-15 23:27:46 -0700 |
commit | 69bbfa98564efc7a8b865f06b01c0e404ac1e658 (patch) | |
tree | 188c18f4c23b986b1b1647738e4e14fe63513ec5 /src/proof/abs/absOut.c | |
parent | ec95f569dd543d6a6acc8b9910cb605f14e59e61 (diff) | |
download | abc-69bbfa98564efc7a8b865f06b01c0e404ac1e658.tar.gz abc-69bbfa98564efc7a8b865f06b01c0e404ac1e658.tar.bz2 abc-69bbfa98564efc7a8b865f06b01c0e404ac1e658.zip |
Created new abstraction package from the code that was all over the place.
Diffstat (limited to 'src/proof/abs/absOut.c')
-rw-r--r-- | src/proof/abs/absOut.c | 458 |
1 files changed, 458 insertions, 0 deletions
diff --git a/src/proof/abs/absOut.c b/src/proof/abs/absOut.c new file mode 100644 index 00000000..c230acb4 --- /dev/null +++ b/src/proof/abs/absOut.c @@ -0,0 +1,458 @@ +/**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; + clock_t clk = 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", 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", 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; +// clock_t clk = 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 + |