diff options
Diffstat (limited to 'src/aig/gia/giaAbs.c')
| -rw-r--r-- | src/aig/gia/giaAbs.c | 553 |
1 files changed, 553 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c new file mode 100644 index 00000000..38e010f1 --- /dev/null +++ b/src/aig/gia/giaAbs.c @@ -0,0 +1,553 @@ +/**CFile**************************************************************** + + FileName [giaAbs.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Counter-example-guided abstraction refinement.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#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 fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This procedure sets default parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p ) +{ + memset( p, 0, sizeof(Gia_ParAbs_t) ); + p->Algo = 0; // algorithm: CBA + p->nFramesMax = 10; // timeframes for PBA + p->nConfMax = 10000; // conflicts for PBA + p->fDynamic = 1; // dynamic unfolding for PBA + p->fConstr = 0; // use constraints + p->nFramesBmc = 250; // timeframes for BMC + p->nConfMaxBmc = 5000; // conflicts for BMC + p->nStableMax = 1000000; // the number of stable frames to quit + p->nRatio = 10; // ratio of flops to quit + p->nBobPar = 1000000; // the number of frames before trying to quit + p->fUseBdds = 0; // use BDDs to refine abstraction + p->fUseDprove = 0; // use 'dprove' to refine abstraction + p->fUseStart = 1; // use starting frame + p->fVerbose = 0; // verbose output + p->fVeryVerbose= 0; // printing additional information + p->Status = -1; // the problem status + p->nFramesDone = -1; // the number of rames covered +} + +/**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 [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 [Performs abstraction on the AIG manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops ) +{ + Gia_Man_t * pGia; + Aig_Man_t * pNew, * pTemp; + pNew = Gia_ManToAig( p, 0 ); + pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops ); + Aig_ManStop( pTemp ); + pGia = Gia_ManFromAig( pNew ); + pGia->vCiNumsOrig = pNew->vCiNumsOrig; + pNew->vCiNumsOrig = NULL; + Aig_ManStop( pNew ); + return pGia; + +} + +/**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 [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars ) +{ + Vec_Int_t * vFlops; + if ( p->vFlopClasses != NULL ) + { + printf( "Gia_ManCexAbstractionStart(): Abstraction latch map is present but will be rederived.\n" ); + Vec_IntFreeP( &p->vFlopClasses ); + } + vFlops = Gia_ManCexAbstractionFlops( p, pPars ); + if ( vFlops ) + { + p->vFlopClasses = Gia_ManFlops2Classes( p, vFlops ); + Vec_IntFree( vFlops ); + } +} + +/**Function************************************************************* + + Synopsis [Derives abstraction using the latch map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ) +{ + Vec_Int_t * vFlops; + Gia_Man_t * pAbs = NULL; + if ( pGia->vFlopClasses == NULL ) + { + printf( "Gia_ManCexAbstractionDerive(): Abstraction latch map is missing.\n" ); + return NULL; + } + vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); + pAbs = Gia_ManCexAbstraction( pGia, vFlops ); + Vec_IntFree( vFlops ); + return pAbs; +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using the latch map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, 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, pCex, 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; +} + +/**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.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Str_t * Gia_ManReadFile( char * pFileName ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Read flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManReadBinary( char * pFileName, char * pToken ) +{ + 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 ) + { + 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; + } + } + Vec_StrFree( vStr ); + return vMap; +} + +/**Function************************************************************* + + Synopsis [Read flop map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; +} + + +/**Function************************************************************* + + Synopsis [Starts abstraction by computing latch map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) +{ + 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 ) + { + fprintf( stdout, "Cannot open intermediate file \"%s\".\n", pFileNameOut ); + return; + } + 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 ) + { + 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 = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 ); + if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) ) + Abc_Print( 1, "Generated counter-example is INVALID.\n" ); + pPars->Status = 0; + } + Vec_IntFreeP( &vCex ); + } +#ifdef WIN32 + _unlink( pFileNameOut ); +#else + unlink( pFileNameOut ); +#endif +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |