From 548e04192bb543890d9f6b4dfef7865d6e5553f6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 7 Sep 2012 20:44:12 -0700 Subject: Updating &gla_refine to perform suffic refinement. --- abclib.dsp | 4 + src/aig/gia/giaAbsGla.c | 210 +------------------------ src/aig/gia/giaAbsOut.c | 400 ++++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/module.make | 1 + src/base/abci/abc.c | 23 ++- 5 files changed, 424 insertions(+), 214 deletions(-) create mode 100644 src/aig/gia/giaAbsOut.c diff --git a/abclib.dsp b/abclib.dsp index 2180e9a4..89ec3bce 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -3419,6 +3419,10 @@ SOURCE=.\src\aig\gia\giaAbsIter.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaAbsOut.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaAbsRef.c # End Source File # Begin Source File diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c index 9b33c066..822a55dd 100644 --- a/src/aig/gia/giaAbsGla.c +++ b/src/aig/gia/giaAbsGla.c @@ -24,7 +24,6 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satSolver2.h" #include "base/main/main.h" -#include "aig/saig/saig.h" ABC_NAMESPACE_IMPL_START @@ -130,220 +129,13 @@ static inline void Gla_ObjClearRef( Rfn_Obj_t * p ) { for ( i = 0; (i < (int)pObj->nFanins) && ((pFanin = Gla_ManObj(p, pObj->Fanins[i])),1); i++ ) // some lessons learned from debugging mismatches between GIA and mapped CNF -// - inputs/output of AND-node maybe PPIs (have SAT vars), but the node is not included in the abstraction +// - inputs/output of AND-node may be PPIs (have SAT vars), but the node is not included in the abstraction // - some logic node can be a PPI of one LUT and an internal node of another LUT //////////////////////////////////////////////////////////////////////// /// 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 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 ); - 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 [Prepares CEX and vMap for refinement.] diff --git a/src/aig/gia/giaAbsOut.c b/src/aig/gia/giaAbsOut.c new file mode 100644 index 00000000..7d0837ec --- /dev/null +++ b/src/aig/gia/giaAbsOut.c @@ -0,0 +1,400 @@ +/**CFile**************************************************************** + + FileName [giaAbsOut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Abstraction refinement outside of abstraction engines.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbsOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "giaAig.h" +#include "aig/saig/saig.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 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 ); + 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 = Abc_InfoHasBit(p->pData, iBit++); + for ( i = 0; 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 [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManTransformFlops( Gia_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vInit ) +{ + Vec_Int_t * vInitNew; + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i, iFlopId; + vInitNew = Vec_IntStart( 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_IntWriteEntry( vInitNew, iFlopId, 1 ); + } + pNew = Gia_ManDupFlip( p, Vec_IntArray(vInitNew) ); + Vec_IntFree( vInitNew ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose ) +{ + Gia_Man_t * pAbs, * pNew; + Vec_Int_t * vPis, * vPPis, * vFlops, * vInit; + 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; + } + // 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 ); + 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 ); + return -1; + } + if ( fVerbose ) + Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" ); + // get inputs + Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, &vFlops, NULL ); + assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) ); + // transform the manager to have new init state + pNew = Gia_ManTransformFlops( p, vFlops, vInit ); + assert( pNew->vGateClasses == NULL ); + pNew->vGateClasses = Vec_IntDup( p->vGateClasses ); + Vec_IntFree( vPis ); + Vec_IntFree( vPPis ); + Vec_IntFree( vFlops ); + Vec_IntFree( vInit ); + // perform abstraction for the new AIG + { + Gia_ParVta_t Pars, * pPars = &Pars; + Gia_VtaSetDefaultParams( pPars ); + pPars->nFramesMax = pCex->iFrame - iFrameStart + 1; + pPars->fVerbose = fVerbose; + RetValue = Ga2_ManPerform( pNew, pPars ); + } + // move the abstraction map + Vec_IntFreeP( &p->vGateClasses ); + p->vGateClasses = pNew->vGateClasses; + pNew->vGateClasses = NULL; + // cleanup + Gia_ManStop( pNew ); + Gia_ManStop( pAbs ); + return -1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index cac2986e..17684032 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -3,6 +3,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaAbsGla.c \ src/aig/gia/giaAbsGla2.c \ src/aig/gia/giaAbsIter.c \ + src/aig/gia/giaAbsOut.c \ src/aig/gia/giaAbsRef.c \ src/aig/gia/giaAbsRef2.c \ src/aig/gia/giaAbsVta.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 25c77048..f24f9e12 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27820,14 +27820,26 @@ usage: ***********************************************************************/ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose ); + extern int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose ); + int iFrameStart = 0; int fMinCut = 1; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF ) { switch ( c ) { + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + iFrameStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrameStart < 0 ) + goto usage; + break; case 'm': fMinCut ^= 1; break; @@ -27855,14 +27867,15 @@ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" ); return 1; } - pAbc->Status = Gia_ManGlaRefine( pAbc->pGia, pAbc->pCex, fMinCut, fVerbose ); + pAbc->Status = Gia_ManNewRefine( pAbc->pGia, pAbc->pCex, iFrameStart, fVerbose ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &gla_refine [-mvh]\n" ); + Abc_Print( -2, "usage: &gla_refine [-F num] [-vh]\n" ); Abc_Print( -2, "\t refines the pre-computed gate map using the counter-example\n" ); - Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" ); + Abc_Print( -2, "\t-F num : starting timeframe for suffix refinement [default = %d]\n", iFrameStart ); +// Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; -- cgit v1.2.3