diff options
Diffstat (limited to 'src/aig/gia/giaAbsGla.c')
| -rw-r--r-- | src/aig/gia/giaAbsGla.c | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c new file mode 100644 index 00000000..5dac89a6 --- /dev/null +++ b/src/aig/gia/giaAbsGla.c @@ -0,0 +1,179 @@ +/**CFile**************************************************************** + + FileName [giaAbsGla.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Gate-level abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbsGla.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.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, Gia_Man_t * pAbs, 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 ) ) + { + printf( "Gia_ManCexRemap(): Counter-example is invalid.\n" ); + Abc_CexFree( pCex ); + pCex = NULL; + } + else + { + printf( "Counter-example verification is successful.\n" ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, 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 ); + extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); + Gia_Man_t * pAbs; + Aig_Man_t * pAig; + Abc_Cex_t * pCare; + Vec_Int_t * vPis, * vPPis; + int f, i, iObjId, nOnes = 0, Counter = 0; + if ( p->vGateClasses == NULL ) + { + printf( "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 ) + { + printf( "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 ) ) + { + printf( "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" ); + Gia_ManStop( pAbs ); + return -1; + } +// else +// printf( "Gia_ManGlaRefine(): The initial counter-example is correct.\n" ); + // get inputs + Gia_GlaCollectInputs( p, p->vGateClasses, &vPis, &vPPis ); + assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); + // minimize the CEX + pAig = Gia_ManToAigSimple( pAbs ); + pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose ); + Aig_ManStop( pAig ); + if ( pCare == NULL ) + printf( "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 ) == 1 ) + continue; + assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 ); + Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 ); +// printf( "Adding object %d.\n", iObjId ); +// Gia_ObjPrint( p, Gia_ManObj(p, iObjId) ); + Counter++; + } + Abc_CexFree( pCare ); + if ( fVerbose ) + printf( "Essential bits = %d. Additional objects = %d.\n", nOnes, Counter ); + // consider the case of SAT + if ( iObjId == -1 ) + { + ABC_FREE( p->pCexSeq ); + p->pCexSeq = Gia_ManCexRemap( p, pAbs, pCex, vPis ); + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Gia_ManStop( pAbs ); + return 0; + } + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Gia_ManStop( pAbs ); + + // extract abstraction to include min-cut + if ( fMinCut ) + Nwk_ManDeriveMinCut( p, fVerbose ); + return -1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |