The-OpenROAD-Project/abc
1
0
Fork 0
mirror of https://github.com/The-OpenROAD-Project/abc.git synced 2026-03-12 11:26:17 +08:00
Code Issues Actions Packages Projects Releases Wiki Activity

Bug fix in CBA and PBA.

Browse Source
This commit is contained in:
Alan Mishchenko
2011-08-18 14:38:02 +07:00
parent 48ae2c448f
commit b71b5bbc23
8 changed files with 46 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
abc.rc
View File

@@ -116,6 +116,7 @@ alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2
alias rwsat "st; rw -l; b -l; rw -l; rf -l"
alias drwsat2 "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf"
alias share "st; multi -m; fx; resyn2"
alias addinit "read_init; undc; strash; zero"
# resubstitution scripts for the IWLS paper
alias src_rw "st; rw -l; rwz -l; rwz -l"

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

@@ -600,7 +600,7 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
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, int * piFrame );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );

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

@@ -316,7 +316,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
@@ -332,7 +332,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo
// refine abstraction using PBA
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose, piFrame );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nStart, nFrames, nConfLimit, fVerbose, piFrame );
// derive new classes
if ( pAig->pSeqModel == NULL )
{

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

@@ -135,7 +135,7 @@ extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t
extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
/*=== sswAbsPba.c ==========================================================*/
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame );
/*=== 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 );

5
src/aig/saig/saigAbsCba.c
View File

@@ -609,7 +609,7 @@ ABC_PRT( "Time", clock() - clk );
***********************************************************************/
Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars )
{
{
Vec_Int_t * vAbsFfsToAdd;
int RetValue, clk = clock();
// assert( pAbs->nRegs > 0 );
@@ -617,6 +617,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
RetValue = Saig_ManBmcScalable( pAbs, pPars );
if ( RetValue == -1 ) // time out - nothing to add
{
printf( "Resource limit is reached during BMC.\n" );
assert( pAbs->pSeqModel == NULL );
return Vec_IntAlloc( 0 );
}
@@ -631,7 +632,7 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
}
if ( pPars->fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) );
printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return vAbsFfsToAdd;

19
src/aig/saig/saigAbsPba.c
View File

@@ -72,7 +72,7 @@ void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pvPiVarMap )
Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec_Int_t ** pvPiVarMap )
{
Aig_Man_t * pFrames; // unrolled timeframes
Vec_Vec_t * vFrameCos; // the list of COs per frame
@@ -80,6 +80,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
Vec_Int_t * vRoots, * vObjs;
Aig_Obj_t * pObj, * pObjNew;
int i, f;
assert( nStart <= nFrames );
// collect COs and Objs visited in each frame
vFrameCos = Vec_VecStart( nFrames );
vFrameObjs = Vec_VecStart( nFrames );
@@ -130,8 +131,11 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
assert( 0 );
}
// create output
Saig_ManForEachPo( pAig, pObj, i )
pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData );
if ( f >= nStart )
{
Saig_ManForEachPo( pAig, pObj, i )
pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData );
}
// transfer
if ( f == nFrames - 1 )
break;
@@ -243,7 +247,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nStart, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
{
Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
Aig_Man_t * pFrames;
@@ -252,10 +256,11 @@ Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int n
Aig_Obj_t * pObj;
int nCoreLits, * pCoreLits;
int i, iVar, RetValue, clk;
if ( fVerbose )
printf( "Performing abstraction with starting frame %d and total number of frames %d.\n", nStart, nFrames );
// create SAT solver
clk = clock();
pFrames = Saig_ManUnrollForPba( pAig, nFrames, &vPiVarMap );
pFrames = Saig_ManUnrollForPba( pAig, nStart, nFrames, &vPiVarMap );
if ( fVerbose )
Aig_ManPrintStats( pFrames );
// pCnf = Cnf_DeriveSimple( pFrames, 0 );
@@ -306,7 +311,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
}
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) );
printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAig)+Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
vFlops = vAbsFfsToAdd;

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

@@ -139,7 +139,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
}
// vFlopsNew contains PI numbers that should be kept in pAbs
if ( fVerbose )
printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) );
printf( "Adding %d registers to the abstraction (total = %d).\n\n", Vec_IntSize(vFlopsNew), Aig_ManRegNum(pAbs)+Vec_IntSize(vFlopsNew) );
// add to the abstraction
Vec_IntForEachEntry( vFlopsNew, Entry, i )
{
@@ -195,7 +195,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
}
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vFlopsNew) );
printf( "Adding %d registers to the abstraction (total = %d). ", Vec_IntSize(vFlopsNew), Aig_ManRegNum(p)+Vec_IntSize(vFlopsNew) );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// vFlopsNew contains PI number that should be kept in pAbs

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

@@ -28438,17 +28438,29 @@ usage:
***********************************************************************/
int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int nStart = 0;
int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
int nConfMax = 100000;
int fVerbose = 0;
int iFrame = -1;
int nConfMax = 10000000;
int fVerbose = 0;
int iFrame = -1;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
nStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nStart < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
@@ -28495,15 +28507,21 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The flop map is not given.\n" );
return 0;
}
Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose, &iFrame );
if ( nStart >= nFramesMax )
{
Abc_Print( -1, "The starting frame (%d) should be less than the total number of frames (%d).\n", nStart, nFramesMax );
return 0;
}
Gia_ManPbaPerform( pAbc->pGia, nStart, nFramesMax, nConfMax, fVerbose, &iFrame );
if ( iFrame >= 0 )
pAbc->nFrames = iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &abs_pba [-FC num] [-vh]\n" );
Abc_Print( -2, "usage: &abs_pba [-SFC num] [-vh]\n" );
Abc_Print( -2, "\t refines abstracted flop map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting timeframe for SAT check [default = %d]\n", nStart );
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" );