diff options
Diffstat (limited to 'src/aig/gia/giaAbs.c')
| -rw-r--r-- | src/aig/gia/giaAbs.c | 359 |
1 files changed, 82 insertions, 277 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 7c20851d..7a4e51f4 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -20,24 +20,14 @@ #include "gia.h" #include "giaAig.h" -#include "giaAbs.h" #include "saig.h" -#ifndef _WIN32 -#include <unistd.h> -#endif - ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Vec_Int_t * Saig_ManProofAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); -extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); -extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -147,50 +137,6 @@ Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops ) /**Function************************************************************* - Synopsis [Computes abstracted flops for the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManCexAbstractionFlops( Gia_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - Aig_Man_t * pNew; - pNew = Gia_ManToAig( p, 0 ); - vFlops = Saig_ManCexAbstractionFlops( pNew, pPars ); - p->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; - Aig_ManStop( pNew ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Computes abstracted flops for the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManProofAbstractionFlops( Gia_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - Aig_Man_t * pNew; - pNew = Gia_ManToAig( p, 0 ); - vFlops = Saig_ManProofAbstractionFlops( pNew, pPars ); - p->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; - Aig_ManStop( pNew ); - return vFlops; -} - -/**Function************************************************************* - Synopsis [Starts abstraction by computing latch map.] Description [] @@ -200,18 +146,22 @@ Vec_Int_t * Gia_ManProofAbstractionFlops( Gia_Man_t * p, Gia_ParAbs_t * pPars ) SeeAlso [] ***********************************************************************/ -void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars ) +void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) { Vec_Int_t * vFlops; - if ( p->vFlopClasses != NULL ) + Aig_Man_t * pNew; + if ( pGia->vFlopClasses != NULL ) { printf( "Gia_ManCexAbstractionStart(): Abstraction latch map is present but will be rederived.\n" ); - Vec_IntFreeP( &p->vFlopClasses ); + Vec_IntFreeP( &pGia->vFlopClasses ); } - vFlops = Gia_ManCexAbstractionFlops( p, pPars ); + pNew = Gia_ManToAig( pGia, 0 ); + vFlops = Saig_ManCexAbstractionFlops( pNew, pPars ); + pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL; + Aig_ManStop( pNew ); if ( vFlops ) { - p->vFlopClasses = Gia_ManFlops2Classes( p, vFlops ); + pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); Vec_IntFree( vFlops ); } } @@ -278,37 +228,11 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFou return -1; } -/**Function************************************************************* - - Synopsis [Starts abstraction by computing latch map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - if ( pGia->vFlopClasses != NULL ) - { - printf( "Gia_ManProofAbstractionStart(): Abstraction latch map is present but will be rederived.\n" ); - Vec_IntFreeP( &pGia->vFlopClasses ); - } - vFlops = Gia_ManProofAbstractionFlops( pGia, pPars ); - if ( vFlops ) - { - pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops ); - Vec_IntFree( vFlops ); - } -} /**Function************************************************************* - Synopsis [Read flop map.] + Synopsis [Transform flop list into flop map.] Description [] @@ -317,28 +241,19 @@ void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) SeeAlso [] ***********************************************************************/ -Vec_Str_t * Gia_ManReadFile( char * pFileName ) +Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew ) { - FILE * pFile; - Vec_Str_t * vStr; - int c; - pFile = fopen( pFileName, "r" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\".\n", pFileName ); - return NULL; - } - vStr = Vec_StrAlloc( 100 ); - while ( (c = fgetc(pFile)) != EOF ) - Vec_StrPush( vStr, (char)c ); - Vec_StrPush( vStr, '\0' ); - fclose( pFile ); - return vStr; + Vec_Int_t * vSelected; + int i, Entry; + vSelected = Vec_IntAlloc( Vec_IntSize(vFlopsNew) ); + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + Vec_IntPush( vSelected, Vec_IntEntry(vFlops, Entry) ); + return vSelected; } /**Function************************************************************* - Synopsis [Read flop map.] + Synopsis [Derive unrolled timeframes.] Description [] @@ -347,68 +262,45 @@ Vec_Str_t * Gia_ManReadFile( char * pFileName ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_ManReadBinary( char * pFileName, char * pToken ) +int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose ) { - Vec_Int_t * vMap = NULL; - Vec_Str_t * vStr; - char * pStr; - int i, Length; - vStr = Gia_ManReadFile( pFileName ); - if ( vStr == NULL ) - return NULL; - pStr = Vec_StrArray( vStr ); - pStr = strstr( pStr, pToken ); - if ( pStr != NULL ) + Gia_Man_t * pAbs; + Aig_Man_t * pAig; + Vec_Int_t * vFlops, * vFlopsNew, * vSelected; + if ( pGia->vFlopClasses == NULL ) { - pStr += strlen( pToken ); - vMap = Vec_IntAlloc( 100 ); - Length = strlen( pStr ); - for ( i = 0; i < Length; i++ ) - { - if ( pStr[i] == '0' ) - Vec_IntPush( vMap, 0 ); - else if ( pStr[i] == '1' ) - Vec_IntPush( vMap, 1 ); - if ( ('a' <= pStr[i] && pStr[i] <= 'z') || - ('A' <= pStr[i] && pStr[i] <= 'Z') ) - break; - } + printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" ); + return 0; } - Vec_StrFree( vStr ); - return vMap; -} - -/**Function************************************************************* - - Synopsis [Read flop map.] - - Description [] - - SideEffects [] - - SeeAlso [] + // derive abstraction + vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses ); + pAbs = Gia_ManCexAbstraction( pGia, vFlops ); + // refine abstraction using PBA + pAig = Gia_ManToAigSimple( pAbs ); + Gia_ManStop( pAbs ); + vFlopsNew = Saig_ManPbaDerive( pAig, nFrames, nConfLimit, fVerbose ); + Aig_ManStop( pAig ); + // derive new classes + if ( vFlopsNew != NULL ) + { + vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew ); + Vec_IntFree( pGia->vFlopClasses ); + pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); + Vec_IntFree( vSelected ); -***********************************************************************/ -int Gia_ManReadInteger( char * pFileName, char * pToken ) -{ - int Result = -1; - Vec_Str_t * vStr; - char * pStr; - vStr = Gia_ManReadFile( pFileName ); - if ( vStr == NULL ) - return -1; - pStr = Vec_StrArray( vStr ); - pStr = strstr( pStr, pToken ); - if ( pStr != NULL ) - Result = atoi( pStr + strlen(pToken) ); - Vec_StrFree( vStr ); - return Result; + Vec_IntFree( vFlopsNew ); + Vec_IntFree( vFlops ); + return 1; + } + Vec_IntFree( vFlops ); + // found counter-eample for the abstracted model + // or exceeded conflict limit + return 0; } - /**Function************************************************************* - Synopsis [Starts abstraction by computing latch map.] + Synopsis [Derive unrolled timeframes.] Description [] @@ -417,133 +309,46 @@ int Gia_ManReadInteger( char * pFileName, char * pToken ) SeeAlso [] ***********************************************************************/ -void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) +int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p ) { - char BufTimeOut[100]; - char BufTimeOutVT[100]; - char Command[1000]; - char * pFileNameIn = "cex_abstr_in_.aig"; - char * pFileNameOut = "cex_abstr_out_.txt"; - FILE * pFile; - Vec_Int_t * vCex; - int RetValue, clk; - if ( pGia->vFlopClasses != NULL ) - { - printf( "Gia_ManCexAbstractionStartNew(): Abstraction latch map is present but will be rederived.\n" ); - Vec_IntFreeP( &pGia->vFlopClasses ); - } - Gia_WriteAiger( pGia, pFileNameIn, 0, 0 ); - sprintf( BufTimeOut, "-timeout=%d", pPars->TimeOut ); - sprintf( BufTimeOutVT, "-vt=%d", pPars->TimeOutVT ); -//ABC switch => cex_abstr switch -//-cba => <input> <output> -//-pba => ,bmc -pba-soft <input> <output> -//-cba-then-pba => -pba-soft <input> <output> -//-cba-with-pba => -pba <input> <output> - if ( pPars->Algo == 0 ) - { - sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d %s %s %s %s", - pPars->fVerbose? "":"-quiet", - pPars->fVeryVerbose? "-sat-verbosity=1":"", - pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar, - pPars->TimeOut? BufTimeOut : "", - pPars->TimeOutVT? BufTimeOutVT : "", - pFileNameIn, pFileNameOut ); - } - else if ( pPars->Algo == 1 ) - { - sprintf( Command, "cex_abstr %s %s -depth=%d -confl=%d -bob=%d ,bmc -pba-soft %s %s %s %s", - pPars->fVerbose? "":"-quiet", - pPars->fVeryVerbose? "-sat-verbosity=1":"", - pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->nBobPar, - pPars->TimeOut? BufTimeOut : "", - pPars->TimeOutVT? BufTimeOutVT : "", - pFileNameIn, pFileNameOut ); - } - else if ( pPars->Algo == 2 ) - { - sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d -pba-soft %s %s %s %s", - pPars->fVerbose? "":"-quiet", - pPars->fVeryVerbose? "-sat-verbosity=1":"", - pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar, - pPars->TimeOut? BufTimeOut : "", - pPars->TimeOutVT? BufTimeOutVT : "", - pFileNameIn, pFileNameOut ); - } - else if ( pPars->Algo == 3 ) - { - sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d -pba %s %s %s %s", - pPars->fVerbose? "":"-quiet", - pPars->fVeryVerbose? "-sat-verbosity=1":"", - pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar, - pPars->TimeOut? BufTimeOut : "", - pPars->TimeOutVT? BufTimeOutVT : "", - pFileNameIn, pFileNameOut ); - } - else - { - printf( "Unnknown option (algo=%d). CBA (algo=0) is assumed.\n", pPars->Algo ); - sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d %s %s %s %s", - pPars->fVerbose? "":"-quiet", - pPars->fVeryVerbose? "-sat-verbosity=1":"", - pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar, - pPars->TimeOut? BufTimeOut : "", - pPars->TimeOutVT? BufTimeOutVT : "", - pFileNameIn, pFileNameOut ); - } - // run the command - printf( "Executing command line \"%s\"\n", Command ); - clk = clock(); - RetValue = system( Command ); - clk = clock() - clk; -#ifdef WIN32 - _unlink( pFileNameIn ); -#else - unlink( pFileNameIn ); -#endif - if ( RetValue == -1 ) - { - fprintf( stdout, "Command \"%s\" did not succeed.\n", Command ); - return; - } - // check that the input PostScript file is okay - if ( (pFile = fopen( pFileNameOut, "r" )) == NULL ) + Saig_ParBmc_t * pPars = (Saig_ParBmc_t *)p; + Gia_Man_t * pAbs; + Aig_Man_t * pAig; + Vec_Int_t * vFlops, * vFlopsNew, * vSelected; + if ( pGia->vFlopClasses == NULL ) { - fprintf( stdout, "Cannot open intermediate file \"%s\".\n", pFileNameOut ); - return; + printf( "Gia_ManCbaPerform(): Empty abstraction is started.\n" ); + pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); } - fclose( pFile ); - pPars->nFramesDone = Gia_ManReadInteger( pFileNameOut, "depth:" ); - if ( pPars->nFramesDone == -1 ) - printf( "Gia_ManCexAbstractionStartNew(): Cannot read the number of frames covered by BMC.\n" ); - pGia->vFlopClasses = Gia_ManReadBinary( pFileNameOut, "abstraction:" ); - vCex = Gia_ManReadBinary( pFileNameOut, "counter-example:" ); - if ( vCex ) + // derive abstraction + vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses ); + pAbs = Gia_ManCexAbstraction( pGia, vFlops ); + // refine abstraction using PBA + pAig = Gia_ManToAigSimple( pAbs ); + Gia_ManStop( pAbs ); + vFlopsNew = Saig_ManCbaPerform( pAig, pPars ); + Aig_ManStop( pAig ); + // derive new classes + if ( vFlopsNew != NULL ) { - int nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pGia)) / Gia_ManPiNum(pGia); - int nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pGia)) % Gia_ManPiNum(pGia); - if ( nRemain != 0 ) - { - printf( "Counter example has a wrong length.\n" ); - } - else - { - printf( "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 ); - Abc_PrintTime( 1, "Time", clk ); - pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 ); - if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) ) - Abc_Print( 1, "Generated counter-example is INVALID.\n" ); - pPars->Status = 0; - } - Vec_IntFreeP( &vCex ); +// vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew ); + vSelected = NULL; + Vec_IntFree( pGia->vFlopClasses ); + pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); + Vec_IntFree( vSelected ); + + Vec_IntFree( vFlopsNew ); + Vec_IntFree( vFlops ); + return 1; } -#ifdef WIN32 - _unlink( pFileNameOut ); -#else - unlink( pFileNameOut ); -#endif + Vec_IntFree( vFlops ); + // found counter-eample for the abstracted model + // or exceeded conflict limit + return 0; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |