luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improving and updating the abstraction code.

This commit is contained in:
Alan Mishchenko 2011-07-29 15:38:44 +07:00
parent 581daaeade
commit ce38474c74
15 changed files with 1011 additions and 2125 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
abclib.dsp
View File

@ -3487,7 +3487,15 @@ SOURCE=.\src\aig\saig\saigAbs.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbs2.c
SOURCE=.\src\aig\saig\saigAbsCba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsPba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigAbsStart.c
# End Source File
# Begin Source File
@ -3539,10 +3547,6 @@ SOURCE=.\src\aig\saig\saigOutDec.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigPba.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
@ -3787,6 +3791,10 @@ SOURCE=.\src\aig\ssw\sswRarity.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswRarity2.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\ssw\sswSat.c
# End Source File
# Begin Source File

9
src/aig/gia/gia.h
View File

@ -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 );

381
src/aig/gia/giaAbs.c
View File

@ -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 ///
////////////////////////////////////////////////////////////////////////
@ -145,50 +135,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.]
@ -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,9 +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.]
Synopsis [Transform flop list into flop map.]
Description []
@ -289,26 +241,66 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFou
SeeAlso []
***********************************************************************/
void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew )
{
Vec_Int_t * vFlops;
if ( pGia->vFlopClasses != NULL )
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 [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig;
Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
if ( pGia->vFlopClasses == NULL )
{
printf( "Gia_ManProofAbstractionStart(): Abstraction latch map is present but will be rederived.\n" );
Vec_IntFreeP( &pGia->vFlopClasses );
printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
return 0;
}
vFlops = Gia_ManProofAbstractionFlops( pGia, pPars );
if ( vFlops )
// 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 )
{
pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
Vec_IntFree( pGia->vFlopClasses );
pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
Vec_IntFree( vSelected );
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 [Read flop map.]
Synopsis [Derive unrolled timeframes.]
Description []
@ -317,232 +309,45 @@ void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
SeeAlso []
***********************************************************************/
Vec_Str_t * Gia_ManReadFile( char * pFileName )
int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
{
FILE * pFile;
Vec_Str_t * vStr;
int c;
pFile = fopen( pFileName, "r" );
if ( pFile == 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 )
{
printf( "Cannot open file \"%s\".\n", pFileName );
return NULL;
printf( "Gia_ManCbaPerform(): Empty abstraction is started.\n" );
pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
}
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 )
// 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 )
{
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;
}
// 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;
}
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;
Vec_IntFree( vFlops );
// found counter-eample for the abstracted model
// or exceeded conflict limit
return 0;
}
/**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 = 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 );
}
#ifdef WIN32
_unlink( pFileNameOut );
#else
unlink( pFileNameOut );
#endif
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

5
src/aig/saig/module.make
View File

@ -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 \

16
src/aig/saig/saig.h
View File

@ -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 );

364
src/aig/saig/saigAbs.c
View File

@ -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;
}
////////////////////////////////////////////////////////////////////////

237
src/aig/saig/saigAbs2.c
View File

@ -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

56
src/aig/saig/saigAbsCba.c Normal file
View File

@ -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

259
src/aig/saig/saigAbsPba.c Normal file
View File

@ -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

341
src/aig/saig/saigAbsStart.c Normal file
View File

@ -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

752
src/aig/saig/saigPba.c
View File

@ -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

4
src/aig/saig/saigRefSat.c
View File

@ -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

623
src/base/abci/abc.c
View File

@ -45,7 +45,6 @@
#include "retInt.h"
#include "cnf.h"
#include "cec.h"
#include "giaAbs.h"
#include "pdr.h"
#include "tim.h"
@ -247,7 +246,7 @@ static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSim2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSim3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -272,7 +271,6 @@ static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTempor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCegar ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -373,10 +371,11 @@ static int Abc_CommandAbc9Speedup ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsStartNew ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsDerive ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsRefine ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PbaStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PbaStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -668,7 +667,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "sim2", Abc_CommandSim2, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "sim3", Abc_CommandSim3, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 );
@ -698,7 +697,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 );
Cmd_CommandAdd( pAbc, "Verification", "tempor", Abc_CommandTempor, 1 );
Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 );
Cmd_CommandAdd( pAbc, "Verification", "abs", Abc_CommandCegar, 1 );
Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 );
Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 );
@ -794,10 +792,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&era", Abc_CommandAbc9Era, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dch", Abc_CommandAbc9Dch, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_start", Abc_CommandAbc9AbsStart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_newstart", Abc_CommandAbc9AbsStartNew, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_derive", Abc_CommandAbc9AbsDerive, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_refine", Abc_CommandAbc9AbsRefine, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&pba_start", Abc_CommandAbc9PbaStart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&abs_cba", Abc_CommandAbc9AbsCba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 );
@ -15792,7 +15790,7 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandSim2( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
@ -15896,7 +15894,7 @@ int Abc_CommandSim2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: sim2 [-FWBRT num] [-vh]\n" );
Abc_Print( -2, "usage: sim3 [-FWBRT num] [-vh]\n" );
Abc_Print( -2, "\t performs random simulation of the sequential miter\n" );
Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
@ -19632,134 +19630,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandCegar( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParAbs_t Pars, * pPars = &Pars;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
extern Abc_Ntk_t * Abc_NtkDarCegar( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
Gia_ManAbsSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCRcrpfvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesBmc < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfMaxBmc < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRatio < 0 )
goto usage;
break;
case 'c':
pPars->fConstr ^= 1;
break;
case 'r':
pPars->fUseBdds ^= 1;
break;
case 'p':
pPars->fUseDprove ^= 1;
break;
case 'f':
pPars->fUseStart ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( Abc_NtkIsComb(pNtk) )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
return 0;
}
if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) )
{
Abc_Print( -1, "Wrong value of parameter \"-R <num>\".\n" );
return 0;
}
// modify the current network
pNtkRes = Abc_NtkDarCegar( pNtk, pPars );
if ( pNtkRes == NULL )
{
if ( pNtk->pSeqModel == NULL )
Abc_Print( -1, "Abstraction has failed.\n" );
return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: abs [-FCR num] [-crpfvh]\n" );
Abc_Print( -2, "\t performs counter-example-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
Abc_Print( -2, "\t-c : toggle dynamic addition of constraints [default = %s]\n", pPars->fConstr? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
// Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-p : toggle using \"pdr\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
Abc_Print( -2, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -25291,6 +25161,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// extern int Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
int c;
int nFrames = 20;
int nWords = 50;
@ -25299,9 +25170,10 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
int TimeOut = 0;
int fUseCex = 0;
int fLatchOnly = 0;
int fNewAlgo = 0;
int fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlavh" ) ) != EOF )
{
switch ( c )
{
@ -25366,6 +25238,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
fLatchOnly ^= 1;
break;
case 'a':
fNewAlgo ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -25395,7 +25270,10 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
// pAbc->Status = Abc_NtkDarSeqEquiv2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
if ( fNewAlgo )
pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
else
pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
// pAbc->nFrames = pAbc->pCex->iFrame;
// Abc_FrameReplaceCex( pAbc, &pAbc->pCex );
return 0;
@ -25403,13 +25281,14 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &equiv3 [-FWBRT num] [-xlvh]\n" );
Abc_Print( -2, "\t computes candidate equivalence classes\n" );
Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize );
Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n", nBinSize );
Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds );
Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeOut );
Abc_Print( -2, "\t-x : toggle using the current cex to perform refinement [default = %s]\n", fUseCex? "yes": "no" );
Abc_Print( -2, "\t-l : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "yes": "no" );
Abc_Print( -2, "\t-a : toggle using a new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@ -27930,8 +27809,6 @@ int Abc_CommandAbc9AbsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParAbs_t Pars, * pPars = &Pars;
int c;
extern void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars );
// set defaults
Gia_ManAbsSetDefaultParams( pPars );
Extra_UtilGetoptReset();
@ -28039,272 +27916,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9AbsStartNew( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParAbs_t Pars, * pPars = &Pars;
int c;
extern void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars );
// set defaults
Gia_ManAbsSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "AFSCRBTVrpfvwh" ) ) != EOF )
{
switch ( c )
{
case 'A':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->Algo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->Algo < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesBmc < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStableMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStableMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfMaxBmc < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
pPars->nRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nRatio < 0 )
goto usage;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBobPar = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBobPar < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->TimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->TimeOut < 0 )
goto usage;
break;
case 'V':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
goto usage;
}
pPars->TimeOutVT = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->TimeOutVT < 0 )
goto usage;
break;
case 'r':
pPars->fUseBdds ^= 1;
break;
case 'p':
pPars->fUseDprove ^= 1;
break;
case 'f':
pPars->fUseStart ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsStartNew(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9AbsStartNew(): The AIG is combinational.\n" );
return 0;
}
if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) )
{
Abc_Print( -1, "Abc_CommandAbc9AbsStartNew(): Wrong value of parameter \"-R <num>\".\n" );
return 0;
}
Gia_ManCexAbstractionStartNew( pAbc->pGia, pPars );
pAbc->Status = pPars->Status;
pAbc->nFrames = pPars->nFramesDone;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
if ( pPars->fVerbose )
printf( "Updating ABC solving status to be %d and bmc_frames_done to be %d.\n", pPars->Status, pAbc->nFrames );
return 0;
usage:
Abc_Print( -2, "usage: &abs_newstart [-AFSCBTV num] [-vwh]\n" );
Abc_Print( -2, "\t initializes flop map using cex-based abstraction (by Niklas Een)\n" );
Abc_Print( -2, "\t-A num : selects the algorithm to use [default = %d]\n", pPars->Algo );
Abc_Print( -2, "\t 0 = cba\n" );
Abc_Print( -2, "\t 1 = pba\n" );
Abc_Print( -2, "\t 2 = cba-then-pba\n" );
Abc_Print( -2, "\t 3 = cba-with-pba\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
Abc_Print( -2, "\t-S num : the max number of stable frames for BMC [default = %d]\n", pPars->nStableMax );
Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
Abc_Print( -2, "\t-B num : the max number of frames to wait before trying to quit [default = %d]\n", pPars->nBobPar );
Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeOut );
Abc_Print( -2, "\t-V num : approximate \"virtual time\" limit in seconds (0=infinite) [default = %d]\n", pPars->TimeOutVT );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9PbaStart( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_ParAbs_t Pars, * pPars = &Pars;
int c;
extern void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars );
// set defaults
Gia_ManAbsSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCdvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfMax < 0 )
goto usage;
break;
case 'd':
pPars->fDynamic ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9PbaStart(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9PbaStart(): The AIG is combinational.\n" );
return 0;
}
Gia_ManProofAbstractionStart( pAbc->pGia, pPars );
pAbc->Status = pPars->Status;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &pba_start [-FC num] [-dvh]\n" );
Abc_Print( -2, "\t computes initial flop map using proof-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes for PBA [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", pPars->nConfMax );
// Abc_Print( -2, "\t-G num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
// Abc_Print( -2, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
// Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
Abc_Print( -2, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", pPars->fDynamic? "yes": "no" );
// Abc_Print( -2, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", pPars->fExtend? "yes": "no" );
// Abc_Print( -2, "\t-s : toggle skipping proof-based abstraction [default = %s]\n", pPars->fSkipProof? "yes": "no" );
// Abc_Print( -2, "\t-r : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
// Abc_Print( -2, "\t-p : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
// Abc_Print( -2, "\t-f : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -28320,7 +27931,6 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0;
extern Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
@ -28376,7 +27986,6 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
int fSensePath = 0;
int fVerbose = 0;
extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "tsvh" ) ) != EOF )
{
@ -28426,6 +28035,192 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
int nConfMax = 100000;
int fVerbose = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFramesMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConfMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nConfMax < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
if ( pAbc->pGia->vFlopClasses == NULL )
{
Abc_Print( -1, "The flop map is not given.\n" );
return 0;
}
Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose );
// Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &abs_pba [-FC num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted flop map with proof-based abstraction\n" );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", nConfMax );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Saig_ParBmc_t Pars, * pPars = &Pars;
int c;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = pPars->nStart + 10;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStart < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
pPars->nConfLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nConfLimit < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nTimeOut < 0 )
goto usage;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
return 1;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted flop map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : the time out in seconds [default = %d]\n", pPars->nTimeOut );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

69
src/base/abci/abcDar.c
View File

@ -33,7 +33,6 @@
#include "gia.h"
#include "cec.h"
#include "csw.h"
#include "giaAbs.h"
#include "pdr.h"
ABC_NAMESPACE_IMPL_START
@ -3227,66 +3226,6 @@ ABC_PRT( "Time", clock() - clkTotal );
}
/**Function*************************************************************
Synopsis [Performs proof-based abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarCegar( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
if ( pPars->fConstr )
{
printf( "This option is currently not implemented.\n" );
Aig_ManStop( pMan );
return NULL;
}
if ( pPars->fConstr )
{
if ( Saig_ManDetectConstrTest(pMan) )
{
printf( "Performing abstraction while dynamically adding constraints...\n" );
pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
Aig_ManStop( pTemp );
pMan = Saig_ManConCexAbstraction( pTemp = pMan, pPars );
}
else
{
printf( "Constraints are not available. Performing abstraction w/o constraints.\n" );
pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
}
}
else
pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
if ( pTemp->pSeqModel )
{
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
}
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkAfterTrim( pMan, pNtk );
// pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
// pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Interplates two networks.]
@ -4316,13 +4255,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManCexAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
*/
/*
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Saig_ManDualRail( pTemp = pMan, 1 );

2
src/base/cmd/cmdPlugin.c
View File

@ -560,8 +560,6 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->Status = Abc_ManReadStatus( pFileOut, "result:" );
// get bug-free depth
pAbc->nFrames = Abc_ManReadInteger( pFileOut, "bug-free-depth:" );
// if ( pAbc->nFrames == -1 )
// printf( "Gia_ManCexAbstractionStartNew(): Cannot read the number of frames covered by BMC.\n" );
// get abstraction
pAbc->pGia->vFlopClasses = Abc_ManReadBinary( pFileOut, "abstraction:" );
// get counter-example