From 7629fd6aea2ff9cf27c16b235da7d90bec0f3e7e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 24 Jun 2012 18:45:42 -0700 Subject: Added min-cut-based refinement of gate-level abstraction (command &gla_refine). --- src/aig/gia/gia.h | 1 + src/aig/gia/giaAbsGla.c | 179 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaDup.c | 46 +++++++++++++ src/aig/gia/module.make | 1 + 4 files changed, 227 insertions(+) create mode 100644 src/aig/gia/giaAbsGla.c (limited to 'src/aig/gia') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 1bb883fa..b4ce11e6 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -691,6 +691,7 @@ extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses ); +extern void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); 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 + diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 7d11eff9..a5c246cb 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1783,6 +1783,52 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) return pNew; } +/**Function************************************************************* + + Synopsis [Collects PIs and PPIs of the abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_GlaCollectInputs( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis ) +{ + Vec_Int_t * vAssigned, * vPis, * vPPis; + Gia_Obj_t * pObj; + int i; + assert( Gia_ManPoNum(p) == 1 ); + assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) ); + // create included objects and their fanins + vAssigned = Gia_GlaCollectAssigned( p, vGateClasses ); + // create additional arrays + vPis = Vec_IntAlloc( 1000 ); + vPPis = Vec_IntAlloc( 1000 ); + Gia_ManForEachObjVec( vAssigned, p, pObj, i ) + { + if ( Gia_ObjIsPi(p, pObj) ) + Vec_IntPush( vPis, Gia_ObjId(p,pObj) ); + else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) ) + Vec_IntPush( vPPis, Gia_ObjId(p,pObj) ); + else if ( Gia_ObjIsAnd(pObj) ) + {} + else if ( Gia_ObjIsRo(p, pObj) ) + {} + else assert( Gia_ObjIsConst0(pObj) ); + } + Vec_IntFree( vAssigned ); + if ( pvPis ) + *pvPis = vPis; + else + Vec_IntFree( vPis ); + if ( pvPPis ) + *pvPPis = vPPis; + else + Vec_IntFree( vPPis ); +} + /**Function************************************************************* Synopsis [Returns the array of neighbors.] diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index aec38f40..e54a30d4 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -1,5 +1,6 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAbs.c \ + src/aig/gia/giaAbsGla.c \ src/aig/gia/giaAbsVta.c \ src/aig/gia/giaAig.c \ src/aig/gia/giaAiger.c \ -- cgit v1.2.3