diff options
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/gia/gia.h | 9 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 359 | ||||
-rw-r--r-- | src/aig/saig/module.make | 5 | ||||
-rw-r--r-- | src/aig/saig/saig.h | 16 | ||||
-rw-r--r-- | src/aig/saig/saigAbs.c | 364 | ||||
-rw-r--r-- | src/aig/saig/saigAbs2.c | 237 | ||||
-rw-r--r-- | src/aig/saig/saigAbsCba.c | 56 | ||||
-rw-r--r-- | src/aig/saig/saigAbsPba.c | 259 | ||||
-rw-r--r-- | src/aig/saig/saigAbsStart.c | 341 | ||||
-rw-r--r-- | src/aig/saig/saigPba.c | 752 | ||||
-rw-r--r-- | src/aig/saig/saigRefSat.c | 4 |
11 files changed, 777 insertions, 1625 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 2a8e6664..195abcc9 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -34,6 +34,7 @@ #include "vec.h" #include "utilCex.h" +#include "giaAbs.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -195,8 +196,6 @@ extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars ); static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; } -//static inline int Gia_Float2Int( float Val ) { return *((int *)&Val); } -//static inline float Gia_Int2Float( int Num ) { return *((float *)&Num); } static inline int Gia_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; } static inline float Gia_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; } static inline int Gia_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } @@ -597,6 +596,12 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== giaAbs.c ===========================================================*/ +extern void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars ); +Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); +int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); +extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose ); +extern int Gia_ManCbaPerform( 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 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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make index 454be222..1171bd46 100644 --- a/src/aig/saig/module.make +++ b/src/aig/saig/module.make @@ -1,5 +1,7 @@ SRC += src/aig/saig/saigAbs.c \ - src/aig/saig/saigAbs2.c \ + src/aig/saig/saigAbsCba.c \ + src/aig/saig/saigAbsPba.c \ + src/aig/saig/saigAbsStart.c \ src/aig/saig/saigBmc.c \ src/aig/saig/saigBmc2.c \ src/aig/saig/saigBmc3.c \ @@ -12,7 +14,6 @@ SRC += src/aig/saig/saigAbs.c \ src/aig/saig/saigIoa.c \ src/aig/saig/saigMiter.c \ src/aig/saig/saigOutDec.c \ - src/aig/saig/saigPba.c \ src/aig/saig/saigPhase.c \ src/aig/saig/saigRefSat.c \ src/aig/saig/saigRetFwd.c \ diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 315e3a8a..93375fd8 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -124,13 +124,17 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - + /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ); -/*=== sswAbs2.c ==========================================================*/ -extern Aig_Man_t * Saig_ManConCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ); -/*=== sswPba.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ); +extern Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses ); +extern Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops ); +/*=== sswAbsCba.c ==========================================================*/ +extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ); +/*=== sswAbsPba.c ==========================================================*/ +extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ); +/*=== sswAbsStart.c ==========================================================*/ +extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ); +extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); 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 ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 3cd508a6..0322361a 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -6,7 +6,7 @@ PackageName [Sequential AIG package.] - Synopsis [Counter-example-based abstraction.] + Synopsis [Intergrated abstraction procedure.] Author [Alan Mishchenko] @@ -37,7 +37,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [Collects internal nodes in the DFS order.] + Synopsis [Transform flop map into flop list.] Description [] @@ -46,366 +46,36 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -int Saig_ManFindFirstFlop_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses ) { - int RetValue; - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) - return -1; - Aig_ObjSetTravIdCurrent(p, pObj); - if ( Saig_ObjIsPi(p, pObj) ) - return -1; - if ( Saig_ObjIsLo(p, pObj) ) - { - assert( Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p) ); - return Aig_ObjPioNum(pObj)-Saig_ManPiNum(p); - } - assert( Aig_ObjIsNode(pObj) ); - RetValue = Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin0(pObj) ); - if ( RetValue >= 0 ) - return RetValue; - return Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin1(pObj) ); -} - -/**Function************************************************************* - - Synopsis [Returns the index of the flop that appears in the support.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManFindFirstFlop( Aig_Man_t * p ) -{ - Aig_ManIncrementTravId( p ); - Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); - return Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin0(Aig_ManPo(p, 0)) ); - -} - -/**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 intial counter-example is invalid.\n" ); - else - printf( "Saig_ManCexRemap(): The intial 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 ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) - Aig_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 - { - printf( "Counter-example verification is successful.\n" ); - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, 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_ManForEachPi( 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 ); - 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 ); - } - 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.\n\n", 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_ManPiNum(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_ManDeriveAbstraction( p, vFlops ); -} - -/**Function************************************************************* - - Synopsis [Refines abstraction using one step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ) -{ - Aig_Man_t * pAbs; - Vec_Int_t * vFlopsNew; - int i, Entry, clk = clock(); - pAbs = Saig_ManDeriveAbstraction( 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_ManPiNum(pAbs), Aig_ManPiNum(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. ", Vec_IntSize(vFlopsNew) ); - Abc_PrintTime( 0, "Time", clock() - clk ); - } - // vFlopsNew contains PI number that should be kept in pAbs - // add to the abstraction - Vec_IntForEachEntry( vFlopsNew, Entry, i ) - { - Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); - assert( Entry >= Saig_ManPiNum(p) ); - assert( Entry < Aig_ManPiNum(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_ManSetPioNumbers( 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_ManDeriveAbstraction( 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; - } - } + int i, Entry; + vFlops = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vFlopClasses, Entry, i ) + if ( Entry ) + Vec_IntPush( vFlops, i ); return vFlops; } /**Function************************************************************* - Synopsis [Performs counter-example-based abstraction.] + Synopsis [Transform flop list into flop map.] Description [] SideEffects [] SeeAlso [] - + ***********************************************************************/ -Aig_Man_t * Saig_ManCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops ) { - Vec_Int_t * vFlops; - Aig_Man_t * pAbs = NULL; - vFlops = Saig_ManCexAbstractionFlops( p, pPars ); - // write the final result - if ( vFlops ) - { - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); - Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); - printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); - Vec_IntFree( vFlops ); - } - return pAbs; + Vec_Int_t * vFlopClasses; + int i, Entry; + vFlopClasses = Vec_IntStart( nRegs ); + Vec_IntForEachEntry( vFlops, Entry, i ) + Vec_IntWriteEntry( vFlopClasses, Entry, 1 ); + return vFlopClasses; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigAbs2.c b/src/aig/saig/saigAbs2.c deleted file mode 100644 index a4d0f973..00000000 --- a/src/aig/saig/saigAbs2.c +++ /dev/null @@ -1,237 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigAbs.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Counter-example-based abstraction with constraints.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" -#include "ssw.h" -#include "fra.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -extern int Saig_ManFindFirstFlop( Aig_Man_t * p ); -extern 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 ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Returns the array of constraint numbers that are violated.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManFindViolatedConstrs( Aig_Man_t * p, Abc_Cex_t * pCexAbs ) -{ - Vec_Int_t * vFailed; - Aig_Obj_t * pObj, * pObjRi, * pObjRo; - int * pPoMap, i, k, iBit; - pPoMap = ABC_CALLOC( int, Saig_ManPoNum(p) ); - Aig_ManCleanMarkA(p); - Saig_ManForEachLo( p, pObj, i ) - pObj->fMarkA = 0; - assert( pCexAbs->nBits == pCexAbs->nRegs + (pCexAbs->iFrame + 1) * pCexAbs->nPis ); - for ( i = 0; i <= pCexAbs->iFrame; i++ ) - { - iBit = pCexAbs->nRegs + i * pCexAbs->nPis; - Saig_ManForEachPi( p, pObj, k ) - pObj->fMarkA = Aig_InfoHasBit(pCexAbs->pData, iBit++); - Aig_ManForEachNode( p, pObj, k ) - pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) & - (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj)); - Aig_ManForEachPo( p, pObj, k ) - pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj); - Saig_ManForEachPo( p, pObj, k ) - pPoMap[k] |= pObj->fMarkA; - Saig_ManForEachLiLo( p, pObjRi, pObjRo, k ) - pObjRo->fMarkA = pObjRi->fMarkA; - } - Aig_ManCleanMarkA(p); - // collect numbers of failed constraints - vFailed = Vec_IntAlloc( Saig_ManPoNum(p) ); - Saig_ManForEachPo( p, pObj, k ) - if ( pPoMap[k] ) - Vec_IntPush( vFailed, k ); - ABC_FREE( pPoMap ); - return vFailed; -} - -/**Function************************************************************* - - Synopsis [Computes the flops to remain after abstraction.] - - Description [Updates the set of included constraints.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManConCexAbstractionFlops( Aig_Man_t * pInit, Gia_ParAbs_t * pPars, Vec_Int_t * vConstrs ) -{ - int nUseStart = 0; - Aig_Man_t * pCur, * pAbs, * pTemp; - Vec_Int_t * vFlops, * vFlopsCopy, * vConstrsToAdd; - int i, Entry, iFlop, Iter, clk = clock(), clk2 = clock(); - assert( Aig_ManRegNum(pInit) > 0 ); - if ( pPars->fVerbose ) - printf( "Performing counter-example-based refinement with constraints.\n" ); -// Aig_ManSetPioNumbers( p ); - // create constrained AIG - pCur = Saig_ManDupFoldConstrs( pInit, vConstrs ); - assert( Saig_ManPoNum(pCur) == 1 ); - printf( "cur>>> " ); Aig_ManPrintStats( pCur ); - // start the flop map - iFlop = Saig_ManFindFirstFlop( pCur ); - assert( iFlop >= 0 ); -// vFlops = Vec_IntStartNatural( 1 ); - vFlops = Vec_IntAlloc( 1 ); - Vec_IntPush( vFlops, iFlop ); - // create the abstraction - pAbs = Saig_ManDeriveAbstraction( pCur, vFlops ); - printf( "abs>>> " ); Aig_ManPrintStats( pAbs ); - if ( !pPars->fVerbose ) - { - printf( "Init : " ); - Aig_ManPrintStats( pAbs ); - } - printf( "Refining abstraction...\n" ); - for ( Iter = 0; ; Iter++ ) - { - while ( 1 ) - { - vFlopsCopy = Vec_IntDup( vFlops ); - pTemp = Saig_ManCexRefine( pCur, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone ); - if ( pTemp == NULL ) - { - Vec_IntFree( vFlopsCopy ); - break; - } - vConstrsToAdd = Saig_ManFindViolatedConstrs( pInit, pAbs->pSeqModel ); - if ( Vec_IntSize(vConstrsToAdd) == 0 ) - { - Vec_IntFree( vConstrsToAdd ); - Vec_IntFree( vFlopsCopy ); - break; - } - // add the constraints to the base set - Vec_IntForEachEntry( vConstrsToAdd, Entry, i ) - { -// assert( Vec_IntFind(vConstrs, Entry) == -1 ); - Vec_IntPushUnique( vConstrs, Entry ); - } - printf( "Adding %3d constraints. The total is %3d (out of %3d).\n", - Vec_IntSize(vConstrsToAdd), Vec_IntSize(vConstrs), Saig_ManPoNum(pInit)-1 ); - Vec_IntFree( vConstrsToAdd ); - // update the current one - Aig_ManStop( pCur ); - pCur = Saig_ManDupFoldConstrs( pInit, vConstrs ); - printf( "cur>>> " ); Aig_ManPrintStats( pCur ); - // update the flop map - Vec_IntFree( vFlops ); - vFlops = vFlopsCopy; -// Vec_IntFree( vFlopsCopy ); -// vFlops = vFlops; - // update abstraction - Aig_ManStop( pAbs ); - pAbs = Saig_ManDeriveAbstraction( pCur, vFlops ); - printf( "abs>>> " ); Aig_ManPrintStats( pAbs ); - } - Aig_ManStop( pAbs ); - if ( pTemp == NULL ) - break; - 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(pCur)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(pCur) < 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; - } - } - ABC_FREE( pInit->pSeqModel ); - pInit->pSeqModel = pCur->pSeqModel; - pCur->pSeqModel = NULL; - Aig_ManStop( pCur ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs counter-example-based abstraction.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManConCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops, * vConstrs; - Aig_Man_t * pCur, * pAbs = NULL; - assert( Saig_ManPoNum(p) > 1 ); // should contain constraint outputs - // start included constraints - vConstrs = Vec_IntAlloc( 100 ); - // perform refinement - vFlops = Saig_ManConCexAbstractionFlops( p, pPars, vConstrs ); - // write the final result - if ( vFlops ) - { - pCur = Saig_ManDupFoldConstrs( p, vConstrs ); - pAbs = Saig_ManDeriveAbstraction( pCur, vFlops ); - Aig_ManStop( pCur ); - - Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); - printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); - Vec_IntFree( vFlops ); - } - Vec_IntFree( vConstrs ); - return pAbs; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c new file mode 100644 index 00000000..e14c5e8e --- /dev/null +++ b/src/aig/saig/saigAbsCba.c @@ -0,0 +1,56 @@ +/**CFile**************************************************************** + + FileName [saigAbsCba.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [CEX-based abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigAbsCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derive unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) +{ + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c new file mode 100644 index 00000000..75f38d6c --- /dev/null +++ b/src/aig/saig/saigAbsPba.c @@ -0,0 +1,259 @@ +/**CFile**************************************************************** + + FileName [saigAbsPba.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Sequential AIG package.] + + Synopsis [Proof-based abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: saigAbsPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "saig.h" +#include "cnf.h" +#include "satSolver.h" +#include "giaAig.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collect nodes in the unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots ) +{ + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pAig, pObj); + if ( Aig_ObjIsPo(pObj) ) + Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); + else if ( Aig_ObjIsNode(pObj) ) + { + Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); + Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots ); + } + if ( vRoots && Saig_ObjIsLo( pAig, pObj ) ) + Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) ); + Vec_IntPush( vObjs, Aig_ObjId(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derives unrolled timeframes for PBA.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames ) +{ + Aig_Man_t * pFrames; // unrolled timeframes + Vec_Vec_t * vFrameCos; // the list of COs per frame + Vec_Vec_t * vFrameObjs; // the list of objects per frame + Vec_Int_t * vRoots, * vObjs; + Aig_Obj_t * pObj, * pObjNew; + int i, f; + // collect COs and Objs visited in each frame + vFrameCos = Vec_VecStart( nFrames ); + vFrameObjs = Vec_VecStart( nFrames ); + for ( f = nFrames-1; f >= 0; f-- ) + { + // add POs of this frame + vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f ); + Saig_ManForEachPo( pAig, pObj, i ) + Vec_IntPush( vRoots, Aig_ObjId(pObj) ); + // collect nodes starting from the roots + Aig_ManIncrementTravId( pAig ); + Aig_ManForEachNodeVec( pAig, vRoots, pObj, i ) + Saig_ManUnrollForPba_rec( pAig, pObj, + (Vec_Int_t *)Vec_VecEntry( vFrameObjs, f ), + (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) ); + } + // derive unrolled timeframes + pFrames = Aig_ManStart( 10000 ); + pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + // create activation variables + Saig_ManForEachLo( pAig, pObj, i ) + Aig_ObjCreatePi( pFrames ); + // initialize the flops + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,i), Aig_ObjCreatePi(pFrames), Aig_ManConst0(pFrames) ); + // iterate through the frames + pObjNew = Aig_ManConst0(pFrames); + for ( f = 0; f < nFrames; f++ ) + { + // construct + vObjs = (Vec_Int_t *)Vec_VecEntry( vFrameObjs, f ); + Aig_ManForEachNodeVec( pAig, vObjs, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + else if ( Aig_ObjIsPo(pObj) ) + pObj->pData = Aig_ObjChild0Copy(pObj); + else if ( Saig_ObjIsPi(pAig, pObj) ) + pObj->pData = Aig_ObjCreatePi( pFrames ); + else if ( Aig_ObjIsConst1(pObj) ) + pObj->pData = Aig_ManConst1(pFrames); + else if ( !Saig_ObjIsLo(pAig, pObj) ) + assert( 0 ); + } + // create output + Saig_ManForEachPo( pAig, pObj, i ) + pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData ); + // transfer + if ( f == nFrames - 1 ) + break; + vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f ); + Aig_ManForEachNodeVec( pAig, vRoots, pObj, i ) + { + if ( Saig_ObjIsLi(pAig, pObj) ) + { + int iFlopNum = Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig); + assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) ); + Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,iFlopNum), Aig_ObjCreatePi(pFrames), pObj->pData ); + } + } + } + // cleanup + Vec_VecFree( vFrameCos ); + Vec_VecFree( vFrameObjs ); + // create output + Aig_ObjCreatePo( pFrames, pObjNew ); + Aig_ManSetRegNum( pFrames, 0 ); + // finallize + Aig_ManCleanup( pFrames ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Derive unrolled timeframes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose ) +{ + Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps; + Aig_Man_t * pFrames; + sat_solver * pSat; + Cnf_Dat_t * pCnf; + Aig_Obj_t * pObj; + int nCoreLits, * pCoreLits; + int i, iVar, RetValue, clk; + + // create SAT solver +clk = clock(); + pFrames = Saig_ManUnrollForPba( pAig, nFrames ); +if ( fVerbose ) +Aig_ManPrintStats( pFrames ); + pCnf = Cnf_DeriveSimple( pFrames, 0 ); + pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + if ( pSat == NULL ) + { + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + return NULL; + } +if ( fVerbose ) +Abc_PrintTime( 1, "Preparing", clock() - clk ); + + // map activation variables into flop numbers + vAssumps = Vec_IntAlloc( Aig_ManRegNum(pAig) ); + vMapVar2FF = Vec_IntStartFull( pCnf->nVars ); + Aig_ManForEachPi( pFrames, pObj, i ) + { + if ( i >= Aig_ManRegNum(pAig) ) + break; + iVar = pCnf->pVarNums[Aig_ObjId(pObj)]; + Vec_IntPush( vAssumps, toLitCond(iVar, 1) ); + Vec_IntWriteEntry( vMapVar2FF, iVar, i ); + } + + // run SAT solver +clk = clock(); + RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), + (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +if ( fVerbose ) +Abc_PrintTime( 1, "Solving", clock() - clk ); + if ( RetValue != l_False ) + { + if ( RetValue == l_True ) + printf( "Saig_ManPerformPba(): Internal Error!!! The resulting problem is SAT.\n" ); + else + printf( "Saig_ManPerformPba(): SAT solver timed out.\n" ); + Vec_IntFree( vAssumps ); + Vec_IntFree( vMapVar2FF ); + sat_solver_delete( pSat ); + Aig_ManStop( pFrames ); + Cnf_DataFree( pCnf ); + return NULL; + } + assert( RetValue == l_False ); // UNSAT + + // get relevant SAT literals + nCoreLits = sat_solver_final( pSat, &pCoreLits ); + assert( nCoreLits > 0 ); + if ( fVerbose ) + printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n", + nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts ); + + // collect flops + vFlops = Vec_IntAlloc( nCoreLits ); + for ( i = 0; i < nCoreLits; i++ ) + { + iVar = Vec_IntEntry( vMapVar2FF, lit_var(pCoreLits[i]) ); + assert( iVar >= 0 && iVar < Aig_ManRegNum(pAig) ); + Vec_IntPush( vFlops, iVar ); + } + Vec_IntSort( vFlops, 0 ); + + // cleanup + Vec_IntFree( vAssumps ); + Vec_IntFree( vMapVar2FF ); + sat_solver_delete( pSat ); + Cnf_DataFree( pCnf ); + Aig_ManStop( pFrames ); + return vFlops; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c new file mode 100644 index 00000000..6ec2c21d --- /dev/null +++ b/src/aig/saig/saigAbsStart.c @@ -0,0 +1,341 @@ +/**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 "ssw.h" +#include "fra.h" +#include "bbr.h" +#include "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_ManForEachPi( p, pObj, i ) + { + if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) ) + return i; + } + return -1; +} + +/**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 intial counter-example is invalid.\n" ); + else + printf( "Saig_ManCexRemap(): The intial 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 ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) + Aig_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 + { + printf( "Counter-example verification is successful.\n" ); + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + } + return pCex; +} + +/**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 ); + 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 ); + } + 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.\n\n", 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_ManPiNum(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_ManDeriveAbstraction( p, vFlops ); +} + +/**Function************************************************************* + + Synopsis [Refines abstraction using one step.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose ) +{ + Aig_Man_t * pAbs; + Vec_Int_t * vFlopsNew; + int i, Entry, clk = clock(); + pAbs = Saig_ManDeriveAbstraction( 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_ManPiNum(pAbs), Aig_ManPiNum(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. ", Vec_IntSize(vFlopsNew) ); + Abc_PrintTime( 0, "Time", clock() - clk ); + } + // vFlopsNew contains PI number that should be kept in pAbs + // add to the abstraction + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + { + Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); + assert( Entry >= Saig_ManPiNum(p) ); + assert( Entry < Aig_ManPiNum(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_ManSetPioNumbers( 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_ManDeriveAbstraction( 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 + diff --git a/src/aig/saig/saigPba.c b/src/aig/saig/saigPba.c deleted file mode 100644 index 65b39fc0..00000000 --- a/src/aig/saig/saigPba.c +++ /dev/null @@ -1,752 +0,0 @@ -/**CFile**************************************************************** - - FileName [saigPba.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Sequential AIG package.] - - Synopsis [Proof-based abstraction.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: saigPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "saig.h" - -#include "cnf.h" -#include "satSolver.h" -#include "satStore.h" -#include "ssw.h" -#include "ioa.h" -#include "fra.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static inline char Saig_AbsVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { return Vec_StrGetEntry( p, nObjs*i+pObj->Id ); } -static inline void Saig_AbsSetVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { Vec_StrSetEntry( p, nObjs*i+pObj->Id, (char)1 ); } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Finds the set of clauses involved in the UNSAT core.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue ) -{ - Vec_Int_t * vCore; - void * pSatCnf; - Intp_Man_t * pManProof; - int RetValue, clk = clock(); - *piRetValue = -1; - // solve the problem - RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( RetValue == l_Undef ) - { - printf( "Conflict limit is reached.\n" ); - return NULL; - } - if ( RetValue == l_True ) - { - printf( "The BMC problem is SAT.\n" ); - *piRetValue = 0; - return NULL; - } - if ( fVerbose ) - { - printf( "SAT solver returned UNSAT after %d conflicts. ", pSat->stats.conflicts ); - ABC_PRT( "Time", clock() - clk ); - } - assert( RetValue == l_False ); - pSatCnf = sat_solver_store_release( pSat ); - // derive the UNSAT core - clk = clock(); - pManProof = Intp_ManAlloc(); - vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 ); - Intp_ManFree( pManProof ); - Sto_ManFree( (Sto_Man_t *)pSatCnf ); - if ( fVerbose ) - { - printf( "SAT core contains %d clauses (out of %d). ", Vec_IntSize(vCore), pSat->stats.clauses ); - ABC_PRT( "Time", clock() - clk ); - } - return vCore; -} - - -/**Function************************************************************* - - Synopsis [Mark visited nodes recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * pObj, int i ) -{ - if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ) ) - return 1; - Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ); - if ( Saig_ObjIsPi( p, pObj ) ) - return 1; - if ( Saig_ObjIsLo( p, pObj ) ) - { - if ( i == 0 ) - return 1; - return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 ); - } - if ( Aig_ObjIsPo( pObj ) ) - return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); - Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i ); - Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin1(pObj), i ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Mark visited nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax ) -{ - Vec_Str_t * vObj2Visit; - Aig_Obj_t * pObj; - int i, f; - vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax ); -// Saig_ManForEachLo( p, pObj, i ) -// Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); - for ( f = 0; f < nFramesMax; f++ ) - { - Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f ); - Saig_ManForEachPo( p, pObj, i ) - Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f ); - } - return vObj2Visit; -} - -/**Function************************************************************* - - Synopsis [Performs the actual construction of the output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj ) -{ - if ( pObj->pData ) - return (Aig_Obj_t *)pObj->pData; - assert( Aig_ObjIsNode(pObj) ); - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) ); - return (Aig_Obj_t *)(pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); -} - -/**Function************************************************************* - - Synopsis [Derives a vector of AIG managers, one for each frame.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose ) -{ - Vec_Ptr_t * vFrames, * vLoObjs, * vLiObjs; - Vec_Str_t * vObj2Visit; - Aig_Man_t * pFrame; - Aig_Obj_t * pObj; - int f, i; - vObj2Visit = Saig_AbsMarkVisited( p, nFramesMax ); - vFrames = Vec_PtrAlloc( nFramesMax ); - vLoObjs = Vec_PtrAlloc( 100 ); - vLiObjs = Vec_PtrAlloc( 100 ); - for ( f = 0; f < nFramesMax; f++ ) - { - Aig_ManCleanData( p ); - pFrame = Aig_ManStart( 1000 ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pFrame); - // create PIs - Vec_PtrClear( vLoObjs ); - Vec_PtrClear( vLiObjs ); - Aig_ManForEachPi( p, pObj, i ) - { - if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) - { - pObj->pData = Aig_ObjCreatePi(pFrame); - if ( i >= Saig_ManPiNum(p) ) - Vec_PtrPush( vLoObjs, pObj ); - } - } - // remember the number of (implicit) registers in this frame - pFrame->nAsserts = Vec_PtrSize(vLoObjs); - // create POs - Aig_ManForEachPo( p, pObj, i ) - { - if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) ) - { - Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) ); - pObj->pData = Aig_ObjCreatePo( pFrame, Aig_ObjChild0Copy(pObj) ); - if ( i >= Saig_ManPoNum(p) ) - Vec_PtrPush( vLiObjs, pObj ); - } - } -// Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) ); - Vec_PtrPush( vFrames, Cnf_DeriveSimple(pFrame, Aig_ManPoNum(pFrame)) ); - // set the new PIs to point to the corresponding registers - Aig_ManCleanData( pFrame ); - Vec_PtrForEachEntry( Aig_Obj_t *, vLoObjs, pObj, i ) - ((Aig_Obj_t *)pObj->pData)->pData = pObj; - Vec_PtrForEachEntry( Aig_Obj_t *, vLiObjs, pObj, i ) - ((Aig_Obj_t *)pObj->pData)->pData = pObj; - if ( fVerbose ) - printf( "%3d : PI =%8d. PO =%8d. Flop =%8d. Node =%8d.\n", - f, Aig_ManPiNum(pFrame), Aig_ManPoNum(pFrame), pFrame->nAsserts, Aig_ManNodeNum(pFrame) ); - } - Vec_PtrFree( vLoObjs ); - Vec_PtrFree( vLiObjs ); - Vec_StrFree( vObj2Visit ); - return vFrames; -} - -/**Function************************************************************* - - Synopsis [Derives a vector of AIG managers, one for each frame.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames ) -{ - sat_solver * pSat; - Cnf_Dat_t * pCnf, * pCnfPrev; - Vec_Int_t * vPoLits; - Aig_Obj_t * pObjPo, * pObjLi, * pObjLo; - int f, i, Lit, Lits[2], iVarOld, iVarNew, nSatVars, nRegisters; - // start array of output literals - vPoLits = Vec_IntAlloc( 100 ); - // count the number of CNF variables - nSatVars = 0; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - nSatVars += pCnf->nVars; - - // create the SAT solver - pSat = sat_solver_new(); - sat_solver_store_alloc( pSat ); - sat_solver_setnvars( pSat, nSatVars ); - - // add clauses for the timeframes - nSatVars = 0; -// Vec_PtrForEachEntryReverse( Cnf_Dat_t *, vFrames, pCnf, f ) - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - { - // lift clauses of this CNF - Cnf_DataLift( pCnf, nSatVars ); - nSatVars += pCnf->nVars; - // copy clauses into the manager - for ( i = 0; i < pCnf->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - { - printf( "The BMC problem is trivially UNSAT.\n" ); - sat_solver_delete( pSat ); - Vec_IntFree( vPoLits ); - return NULL; - } - } - // remember output literal - Aig_ManForEachPo( pCnf->pMan, pObjPo, i ) - { - if ( i == Saig_ManPoNum(p) ) - break; - Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) ); - } - } - - // add auxiliary clauses (output, connectors, initial) - // add output clause - if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) ) - { - printf( "SAT solver is not created correctly.\n" ); - assert( 0 ); - } - Vec_IntFree( vPoLits ); - - // add connecting clauses - pCnfPrev = (Cnf_Dat_t *)Vec_PtrEntry( vFrames, 0 ); - Vec_PtrForEachEntryStart( Cnf_Dat_t *, vFrames, pCnf, f, 1 ) - { - nRegisters = pCnf->pMan->nAsserts; - assert( nRegisters <= Aig_ManPoNum(pCnfPrev->pMan) ); - assert( nRegisters <= Aig_ManPiNum(pCnf->pMan) ); - for ( i = 0; i < nRegisters; i++ ) - { - pObjLi = Aig_ManPo( pCnfPrev->pMan, Aig_ManPoNum(pCnfPrev->pMan) - nRegisters + i ); - pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i ); - // get variable numbers - iVarOld = pCnfPrev->pVarNums[pObjLi->Id]; - iVarNew = pCnf->pVarNums[pObjLo->Id]; - // add clauses connecting existing variables - Lits[0] = toLitCond( iVarOld, 0 ); - Lits[1] = toLitCond( iVarNew, 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( iVarOld, 1 ); - Lits[1] = toLitCond( iVarNew, 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - pCnfPrev = pCnf; - } - // add unit clauses - pCnf = (Cnf_Dat_t *)Vec_PtrEntry( vFrames, 0 ); - nRegisters = pCnf->pMan->nAsserts; - for ( i = 0; i < nRegisters; i++ ) - { - pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i ); - assert( pCnf->pVarNums[pObjLo->Id] >= 0 ); - Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - assert( 0 ); - } - sat_solver_store_mark_roots( pSat ); - return pSat; -} - - -/**Function************************************************************* - - Synopsis [Creates SAT solver for BMC.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames ) -{ - sat_solver * pSat; - Vec_Int_t * vPoLits; - Aig_Obj_t * pObjPo, * pObjLi, * pObjLo; - int f, i, Lit, Lits[2], iVarOld, iVarNew; - // start array of output literals - vPoLits = Vec_IntAlloc( nFrames * Saig_ManPoNum(pCnf->pMan) ); - // create the SAT solver - pSat = sat_solver_new(); - sat_solver_store_alloc( pSat ); - sat_solver_setnvars( pSat, pCnf->nVars * nFrames ); - - // add clauses for the timeframes - for ( f = 0; f < nFrames; f++ ) - { - for ( i = 0; i < pCnf->nClauses; i++ ) - { - if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) - { - printf( "The BMC problem is trivially UNSAT.\n" ); - sat_solver_delete( pSat ); - Vec_IntFree( vPoLits ); - return NULL; - } - } - // remember output literal - Saig_ManForEachPo( pCnf->pMan, pObjPo, i ) - Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) ); - // lift CNF to the next frame - Cnf_DataLift( pCnf, pCnf->nVars ); - } - // put CNF back to the original level - Cnf_DataLift( pCnf, - pCnf->nVars * nFrames ); - - // add auxiliary clauses (output, connectors, initial) - // add output clause - if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) ) - assert( 0 ); - Vec_IntFree( vPoLits ); - // add connecting clauses - for ( f = 0; f < nFrames; f++ ) - { - // connect to the previous timeframe - if ( f > 0 ) - { - Saig_ManForEachLiLo( pCnf->pMan, pObjLi, pObjLo, i ) - { - iVarOld = pCnf->pVarNums[pObjLi->Id] - pCnf->nVars; - iVarNew = pCnf->pVarNums[pObjLo->Id]; - // add clauses connecting existing variables - Lits[0] = toLitCond( iVarOld, 0 ); - Lits[1] = toLitCond( iVarNew, 1 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - Lits[0] = toLitCond( iVarOld, 1 ); - Lits[1] = toLitCond( iVarNew, 0 ); - if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) ) - assert( 0 ); - } - } - // lift CNF to the next frame - Cnf_DataLift( pCnf, pCnf->nVars ); - } - // put CNF back to the original level - Cnf_DataLift( pCnf, - pCnf->nVars * nFrames ); - // add unit clauses - Saig_ManForEachLo( pCnf->pMan, pObjLo, i ) - { - assert( pCnf->pVarNums[pObjLo->Id] >= 0 ); - Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 ); - if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) - assert( 0 ); - } - sat_solver_store_mark_roots( pSat ); - return pSat; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec_Int_t * vCore ) -{ - Aig_Obj_t * pObj; - Cnf_Dat_t * pCnf; - Vec_Int_t * vFlops; - int * pVars, * pFlops; - int i, f, iClause, iReg, * piLit, nSatVars, nSatClauses; - // count the number of CNF variables - nSatVars = 0; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - nSatVars += pCnf->nVars; - // mark register variables - pVars = ABC_ALLOC( int, nSatVars ); - for ( i = 0; i < nSatVars; i++ ) - pVars[i] = -1; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - { - Aig_ManForEachPi( pCnf->pMan, pObj, i ) - { - assert( pCnf->pVarNums[pObj->Id] >= 0 ); - assert( pCnf->pVarNums[pObj->Id] < nSatVars ); - if ( pObj->pData == NULL ) - continue; - iReg = Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) - Saig_ManPiNum(p); - assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); - pVars[ pCnf->pVarNums[pObj->Id] ] = iReg; - } - Aig_ManForEachPo( pCnf->pMan, pObj, i ) - { - assert( pCnf->pVarNums[pObj->Id] >= 0 ); - assert( pCnf->pVarNums[pObj->Id] < nSatVars ); - if ( pObj->pData == NULL ) - continue; - iReg = Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) - Saig_ManPoNum(p); - assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); - pVars[ pCnf->pVarNums[pObj->Id] ] = iReg; - } - } - // mark used registers - pFlops = ABC_CALLOC( int, Aig_ManRegNum(p) ); - Vec_IntForEachEntry( vCore, iClause, i ) - { - nSatClauses = 0; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f ) - { - if ( iClause < nSatClauses + pCnf->nClauses ) - break; - nSatClauses += pCnf->nClauses; - } - if ( f == Vec_PtrSize(vFrames) ) - continue; - iClause = iClause - nSatClauses; - assert( iClause >= 0 ); - assert( iClause < pCnf->nClauses ); - // consider the clause - for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ ) - { - iReg = pVars[ lit_var(*piLit) ]; - if ( iReg >= 0 ) - pFlops[iReg] = 1; - } - } - // collect registers - vFlops = Vec_IntAlloc( Aig_ManRegNum(p) ); - for ( i = 0; i < Aig_ManRegNum(p); i++ ) - if ( pFlops[i] ) - Vec_IntPush( vFlops, i ); - ABC_FREE( pFlops ); - ABC_FREE( pVars ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vCore ) -{ - Aig_Obj_t * pObj; - Vec_Int_t * vFlops; - int * pVars, * pFlops; - int i, iClause, iReg, * piLit; - // mark register variables - pVars = ABC_ALLOC( int, pCnf->nVars ); - for ( i = 0; i < pCnf->nVars; i++ ) - pVars[i] = -1; - Saig_ManForEachLi( pCnf->pMan, pObj, i ) - pVars[ pCnf->pVarNums[pObj->Id] ] = i; - Saig_ManForEachLo( pCnf->pMan, pObj, i ) - pVars[ pCnf->pVarNums[pObj->Id] ] = i; - // mark used registers - pFlops = ABC_CALLOC( int, Aig_ManRegNum(pCnf->pMan) ); - Vec_IntForEachEntry( vCore, iClause, i ) - { - // skip auxiliary clauses - if ( iClause >= pCnf->nClauses * nFrames ) - continue; - // consider the clause - iClause = iClause % pCnf->nClauses; - for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ ) - { - iReg = pVars[ lit_var(*piLit) ]; - if ( iReg >= 0 ) - pFlops[iReg] = 1; - } - } - // collect registers - vFlops = Vec_IntAlloc( Aig_ManRegNum(pCnf->pMan) ); - for ( i = 0; i < Aig_ManRegNum(pCnf->pMan); i++ ) - if ( pFlops[i] ) - Vec_IntPush( vFlops, i ); - ABC_FREE( pFlops ); - ABC_FREE( pVars ); - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_AbsFreeCnfs( Vec_Ptr_t * vFrames ) -{ - Cnf_Dat_t * pCnf; - int i; - Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, i ) - { - Aig_ManStop( pCnf->pMan ); - Cnf_DataFree( pCnf ); - } - Vec_PtrFree( vFrames ); -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops ) -{ - Vec_Ptr_t * vFlopPtrs, * vSupp; - Aig_Obj_t * pObj; - int i, Entry; - // collect latch inputs - vFlopPtrs = Vec_PtrAlloc( 1000 ); - Vec_IntForEachEntry( vFlops, Entry, i ) - { - Vec_PtrPush( vFlopPtrs, Saig_ManLi(p, Entry) ); - pObj = Saig_ManLo(p, Entry); - pObj->fMarkA = 1; - } - // collect latch outputs - vSupp = Vec_PtrAlloc( 1000 ); - Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vFlopPtrs), Vec_PtrSize(vFlopPtrs), vSupp ); - Vec_PtrFree( vFlopPtrs ); - // mark influencing flops - Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i ) - pObj->fMarkA = 1; - Vec_PtrFree( vSupp ); - // reload flops - Vec_IntClear( vFlops ); - Aig_ManForEachPi( p, pObj, i ) - { - if ( pObj->fMarkA == 0 ) - continue; - pObj->fMarkA = 0; - if ( Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) >= 0 ) - Vec_IntPush( vFlops, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); - } -} - - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Saig_ManProofAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - sat_solver * pSat; - Vec_Ptr_t * vFrames = NULL; - Vec_Int_t * vCore; - Cnf_Dat_t * pCnf = NULL; - int clk = clock(), clk2 = clock(); - if ( pPars->fVerbose ) - printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax ); - assert( Aig_ManRegNum(p) > 0 ); - Aig_ManSetPioNumbers( p ); - if ( pPars->fDynamic ) - { - // create CNF for the frames - vFrames = Saig_AbsCreateFrames( p, pPars->nFramesMax, pPars->fVerbose ); - // create dynamic solver - pSat = Saig_AbsCreateSolverDyn( p, vFrames ); - } - else - { - // create CNF for the AIG - pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); - // create SAT solver for the unrolled AIG - pSat = Saig_AbsCreateSolver( pCnf, pPars->nFramesMax ); - } - if ( pPars->fVerbose ) - { - printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); - ABC_PRT( "Time", clock() - clk2 ); - } - // compute UNSAT core - vCore = Saig_AbsSolverUnsatCore( pSat, pPars->nConfMax, pPars->fVerbose, &pPars->Status ); - sat_solver_delete( pSat ); - if ( vCore == NULL ) - { - if ( vFrames ) - Saig_AbsFreeCnfs( vFrames ); - return NULL; - } - pPars->nFramesDone = pPars->nFramesMax; - // collect registers - if ( pPars->fDynamic ) - { - vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); - Saig_AbsFreeCnfs( vFrames ); - } - else - { - vFlops = Saig_AbsCollectRegisters( pCnf, pPars->nFramesMax, vCore ); - Cnf_DataFree( pCnf ); - } - Vec_IntFree( vCore ); - if ( pPars->fVerbose ) - { - printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); - ABC_PRT( "Time", clock() - clk ); - } - return vFlops; -} - -/**Function************************************************************* - - Synopsis [Performs proof-based abstraction using BMC of the given depth.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) -{ - Vec_Int_t * vFlops; - Aig_Man_t * pAbs = NULL; - vFlops = Saig_ManProofAbstractionFlops( p, pPars ); - // write the final result - if ( vFlops ) - { - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); - Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); - printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); - Vec_IntFree( vFlops ); - } - return pAbs; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index 0b3dff23..27c243b5 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.c @@ -294,10 +294,10 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu } // derive unrolled timeframes - pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * (pCex->iFrame+1) ); + pFrames = Aig_ManStart( 10000 ); pFrames->pName = Aig_UtilStrsav( pAig->pName ); pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); - // initialize the flops of + // initialize the flops Saig_ManForEachLo( pAig, pObj, i ) pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, i) ); // iterate through the frames |