diff options
Diffstat (limited to 'src/proof/abs/absOldRef.c')
| -rw-r--r-- | src/proof/abs/absOldRef.c | 369 |
1 files changed, 369 insertions, 0 deletions
diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c new file mode 100644 index 00000000..dee28cad --- /dev/null +++ b/src/proof/abs/absOldRef.c @@ -0,0 +1,369 @@ +/**CFile**************************************************************** + + FileName [saigAbsStart.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Counter-example-based abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigAbsStart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abs.h" +#include "proof/ssw/ssw.h" +#include "proof/fra/fra.h" +#include "proof/bbr/bbr.h" +#include "proof/pdr/pdr.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derive a new counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs ) +{ + Abc_Cex_t * pCex; + Aig_Obj_t * pObj; + int i, f; + if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) ) + printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" ); +// else +// printf( "Saig_ManCexRemap(): The initial counter-example is correct.\n" ); + // start the counter-example + pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 ); + pCex->iFrame = pCexAbs->iFrame; + pCex->iPo = pCexAbs->iPo; + // copy the bit data + for ( f = 0; f <= pCexAbs->iFrame; f++ ) + { + Saig_ManForEachPi( pAbs, pObj, i ) + { + if ( i == Saig_ManPiNum(p) ) + break; + if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) + Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i ); + } + } + // verify the counter example + if ( !Saig_ManVerifyCex( p, pCex ) ) + { + printf( "Saig_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 [Find the first PI corresponding to the flop.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) +{ + Aig_Obj_t * pObj; + int i; + assert( pAbs->vCiNumsOrig != NULL ); + Aig_ManForEachCi( p, pObj, i ) + { + if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) ) + return i; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using one step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames ) +{ + Vec_Int_t * vFlopsNew; + int i, Entry, RetValue; + *piRetValue = -1; + if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 ) + { +/* + Fra_Sec_t SecPar, * pSecPar = &SecPar; + Fra_SecSetDefaultParams( pSecPar ); + pSecPar->fVerbose = fVerbose; + RetValue = Fra_FraigSec( pAbs, pSecPar, NULL ); +*/ + Abc_Cex_t * pCex = NULL; + Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs ); + Pdr_Par_t Pars, * pPars = &Pars; + Pdr_ManSetDefaultParams( pPars ); + pPars->nTimeOut = 10; + pPars->fVerbose = fVerbose; + if ( pPars->fVerbose ) + printf( "Running property directed reachability...\n" ); + RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex ); + if ( pCex ) + pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex ); + Aig_ManStop( pAbsOrpos ); + pAbs->pSeqModel = pCex; + if ( RetValue ) + *piRetValue = 1; + + } + else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) ) + { + Saig_ParBbr_t Pars, * pPars = &Pars; + Bbr_ManSetDefaultParams( pPars ); + pPars->TimeLimit = 0; + pPars->nBddMax = 1000000; + pPars->nIterMax = nFrames; + pPars->fPartition = 1; + pPars->fReorder = 1; + pPars->fReorderImage = 1; + pPars->fVerbose = fVerbose; + pPars->fSilent = 0; + RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars ); + if ( RetValue ) + *piRetValue = 1; + } + else + { + Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 ); + } + if ( pAbs->pSeqModel == NULL ) + return NULL; + if ( pnUseStart ) + *pnUseStart = pAbs->pSeqModel->iFrame; +// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); + if ( vFlopsNew == NULL ) + return NULL; + if ( Vec_IntSize(vFlopsNew) == 0 ) + { + printf( "Discovered a true counter-example!\n" ); + p->pSeqModel = Saig_ManCexRemap( p, pAbs, pAbs->pSeqModel ); + Vec_IntFree( vFlopsNew ); + *piRetValue = 0; + return NULL; + } + // vFlopsNew contains PI numbers that should be kept in pAbs + if ( fVerbose ) + printf( "Adding %d registers to the abstraction (total = %d).\n\n", Vec_IntSize(vFlopsNew), Aig_ManRegNum(pAbs)+Vec_IntSize(vFlopsNew) ); + // add to the abstraction + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + { + Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); + assert( Entry >= Saig_ManPiNum(p) ); + assert( Entry < Aig_ManCiNum(p) ); + Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); + } + Vec_IntFree( vFlopsNew ); + + Vec_IntSort( vFlops, 0 ); + Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) + assert( Vec_IntEntry(vFlops, i-1) != Entry ); + + return Saig_ManDupAbstraction( p, vFlops ); +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using one step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopClasses, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ) +{ + Aig_Man_t * pAbs; + Vec_Int_t * vFlopsNew; + int i, Entry; + clock_t clk = clock(); + pAbs = Saig_ManDupAbstraction( p, vFlops ); + if ( fSensePath ) + vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); + else +// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); + if ( vFlopsNew == NULL ) + { + Aig_ManStop( pAbs ); + return 0; + } + if ( Vec_IntSize(vFlopsNew) == 0 ) + { + printf( "Refinement did not happen. Discovered a true counter-example.\n" ); + printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAbs), Aig_ManCiNum(p) ); + p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex ); + Vec_IntFree( vFlopsNew ); + Aig_ManStop( pAbs ); + return 0; + } + if ( fVerbose ) + { + printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } + // vFlopsNew contains PI numbers that should be kept in pAbs + // select the most useful flops among those to be added + if ( nFfToAddMax > 0 && Vec_IntSize(vFlopsNew) > nFfToAddMax ) + { + Vec_Int_t * vFlopsNewBest; + // shift the indices + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + Vec_IntAddToEntry( vFlopsNew, i, -Saig_ManPiNum(p) ); + // create new flops + vFlopsNewBest = Saig_ManCbaFilterFlops( p, pCex, vFlopClasses, vFlopsNew, nFfToAddMax ); + assert( Vec_IntSize(vFlopsNewBest) == nFfToAddMax ); + printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vFlopsNew), Vec_IntSize(vFlopsNewBest) ); + // update + Vec_IntFree( vFlopsNew ); + vFlopsNew = vFlopsNewBest; + // shift the indices + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + Vec_IntAddToEntry( vFlopsNew, i, Saig_ManPiNum(p) ); + } + // add to the abstraction + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + { + Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); + assert( Entry >= Saig_ManPiNum(p) ); + assert( Entry < Aig_ManCiNum(p) ); + Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); + } + Vec_IntFree( vFlopsNew ); + Aig_ManStop( pAbs ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Transform flop map into flop list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses ) +{ + Vec_Int_t * vFlops; + int i, Entry; + vFlops = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vFlopClasses, Entry, i ) + if ( Entry ) + Vec_IntPush( vFlops, i ); + return vFlops; +} + +/**Function************************************************************* + + Synopsis [Transform flop list into flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManFlops2Classes( Gia_Man_t * pGia, Vec_Int_t * vFlops ) +{ + Vec_Int_t * vFlopClasses; + int i, Entry; + vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); + Vec_IntForEachEntry( vFlops, Entry, i ) + Vec_IntWriteEntry( vFlopClasses, Entry, 1 ); + return vFlopClasses; +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using the latch map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ) +{ + Aig_Man_t * pNew; + Vec_Int_t * vFlops; + if ( pGia->vFlopClasses == NULL ) + { + printf( "Gia_ManCexAbstractionRefine(): Abstraction latch map is missing.\n" ); + return -1; + } + pNew = Gia_ManToAig( pGia, 0 ); + vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); + if ( !Saig_ManCexRefineStep( pNew, vFlops, pGia->vFlopClasses, pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose ) ) + { + pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; + Vec_IntFree( vFlops ); + Aig_ManStop( pNew ); + return 0; + } + Vec_IntFree( pGia->vFlopClasses ); + pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); + Vec_IntFree( vFlops ); + Aig_ManStop( pNew ); + return -1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |