From 69bbfa98564efc7a8b865f06b01c0e404ac1e658 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 15 Sep 2012 23:27:46 -0700 Subject: Created new abstraction package from the code that was all over the place. --- src/aig/saig/saigAbsStart.c | 310 -------------------------------------------- 1 file changed, 310 deletions(-) delete mode 100644 src/aig/saig/saigAbsStart.c (limited to 'src/aig/saig/saigAbsStart.c') diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c deleted file mode 100644 index 90efef26..00000000 --- a/src/aig/saig/saigAbsStart.c +++ /dev/null @@ -1,310 +0,0 @@ -/**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 "saig.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 [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 ) -{ - extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent ); - 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 [Computes the flops to remain after abstraction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) -{ - int nUseStart = 0; - Aig_Man_t * pAbs, * pTemp; - Vec_Int_t * vFlops; - int Iter;//, clk = clock(), clk2 = clock();//, iFlop; - assert( Aig_ManRegNum(p) > 0 ); - if ( pPars->fVerbose ) - printf( "Performing counter-example-based refinement.\n" ); - Aig_ManSetCioIds( p ); - vFlops = Vec_IntStartNatural( 1 ); -/* - iFlop = Saig_ManFindFirstFlop( p ); - assert( iFlop >= 0 ); - vFlops = Vec_IntAlloc( 1 ); - Vec_IntPush( vFlops, iFlop ); -*/ - // create the resulting AIG - pAbs = Saig_ManDupAbstraction( p, vFlops ); - if ( !pPars->fVerbose ) - { - printf( "Init : " ); - Aig_ManPrintStats( pAbs ); - } - printf( "Refining abstraction...\n" ); - for ( Iter = 0; ; Iter++ ) - { - pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone ); - if ( pTemp == NULL ) - { - ABC_FREE( p->pSeqModel ); - p->pSeqModel = pAbs->pSeqModel; - pAbs->pSeqModel = NULL; - Aig_ManStop( pAbs ); - break; - } - Aig_ManStop( pAbs ); - pAbs = pTemp; - printf( "ITER %4d : ", Iter ); - if ( !pPars->fVerbose ) - Aig_ManPrintStats( pAbs ); - // output the intermediate result of abstraction - Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); -// printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); - // check if the ratio is reached - if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio ) - { - printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); - Aig_ManStop( pAbs ); - pAbs = NULL; - Vec_IntFree( vFlops ); - vFlops = NULL; - break; - } - } - return vFlops; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - -- cgit v1.2.3