diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-25 18:32:06 +0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-10-25 18:32:06 +0800 |
commit | 0f77840520775cd9ac4bdf4cae2813dadc67ae4e (patch) | |
tree | 726ac7c31dd4756fcfdf2701237d4d90912b3700 /src/aig/gia | |
parent | f7fd32978797ed376086d56a83afdd8b30b8efae (diff) | |
download | abc-0f77840520775cd9ac4bdf4cae2813dadc67ae4e.tar.gz abc-0f77840520775cd9ac4bdf4cae2813dadc67ae4e.tar.bz2 abc-0f77840520775cd9ac4bdf4cae2813dadc67ae4e.zip |
New proof-based abstraction code.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 40 |
2 files changed, 40 insertions, 3 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 5f2b94a4..d3165526 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -603,7 +603,8 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); -extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf ); +extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ); +extern int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ); /*=== giaAiger.c ===========================================================*/ extern int Gia_FileSize( char * pFileName ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index ba50b238..54b65484 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -379,7 +379,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit ***********************************************************************/ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) { - extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose ); + extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose ); Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; Vec_Int_t * vGateClasses; Aig_Man_t * pAig; @@ -393,7 +393,43 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf ) */ // perform abstraction pAig = Gia_ManToAigSimple( pGia ); - vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose ); + vGateClasses = Aig_Gla1ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose ); + Aig_ManStop( pAig ); + + // update the map + Vec_IntFreeP( &pGia->vGateClasses ); + pGia->vGateClasses = vGateClasses; + return 1; +} + +/**Function************************************************************* + + Synopsis [Derive unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars ) +{ + extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose ); + Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars; + Vec_Int_t * vGateClasses; + Aig_Man_t * pAig; +/* + // check if flop classes are given + if ( pGia->vGateClasses == NULL ) + { + Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" ); + pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) ); + } +*/ + // perform abstraction + pAig = Gia_ManToAigSimple( pGia ); + vGateClasses = Aig_Gla2ManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose ); Aig_ManStop( pAig ); // update the map |