Skip to content

A
abc
Commit 48ae2c44 by Alan Mishchenko
Options

Bug fix in CBA and PBA.

parent 23671d65
Showing with 86 additions and 33 deletions
src/aig/gia/gia.h
......@@ -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 );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, 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 );
......
src/aig/gia/giaAbs.c
......@@ -268,8 +268,9 @@ void Gia_ManFlopsAddToClasses( Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAd
SeeAlso []
***********************************************************************/
int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
{
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
Vec_Int_t * vAbsFfsToAdd;
......@@ -315,7 +316,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
SeeAlso []
***********************************************************************/
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
{
Gia_Man_t * pAbs;
Aig_Man_t * pAig, * pOrig;
......@@ -331,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 );
vFlopsNew = Saig_ManPbaDerive( pAig, Gia_ManPiNum(pGia), nFrames, nConfLimit, fVerbose, piFrame );
// derive new classes
if ( pAig->pSeqModel == NULL )
{
......
src/aig/saig/saig.h
......@@ -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 );
extern Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, 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 );
......
src/aig/saig/saigAbs.c
......@@ -91,9 +91,9 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
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" );
printf( "Saig_ManCexRemap(): The initial counter-example is invalid.\n" );
// else
// printf( "Saig_ManCexRemap(): The initial 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;
......
src/aig/saig/saigAbsCba.c
......@@ -180,6 +180,8 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
return;
Aig_ObjSetTravIdCurrent(p, pObj);
if ( Aig_ObjIsConst1(pObj) )
return;
if ( Aig_ObjIsPi(pObj) )
{
Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) );
......@@ -267,7 +269,7 @@ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
Aig_ManIncrementTravId( p->pFrames );
Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
Vec_IntFree( vPrios );
assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
// assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
return vReasons;
}
......@@ -630,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) );
Abc_PrintTime( 0, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", clock() - clk );
}
return vAbsFfsToAdd;
}
......
src/aig/saig/saigAbsPba.c
......@@ -171,19 +171,63 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames, Vec_Int_t ** pv
Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vPiVarMap )
{
Abc_Cex_t * pCex;
int i, f, Entry;
pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int i, f, Entry, iBit = 0;
pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
pCex->iPo = -1;
pCex->iFrame = -1;
Vec_IntForEachEntry( vPiVarMap, Entry, i )
{
if ( Entry >= 0 )
{
int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ];
if ( sat_solver_var_value( pSat, iSatVar ) )
Aig_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i );
}
}
// check what frame has failed
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++);
for ( f = 0; f < nFrames; f++ )
{
// Aig_ManForEach
// compute new state
Saig_ManForEachPi( pAig, pObj, i )
pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++);
Aig_ManForEachNode( pAig, pObj, i )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachPo( pAig, pObj, i )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
pObjRo->fMarkB = pObjRi->fMarkB;
// check the outputs
Saig_ManForEachPo( pAig, pObj, i )
{
if ( pObj->fMarkB )
{
pCex->iPo = i;
pCex->iFrame = f;
pCex->nBits = pCex->nRegs + pCex->nPis * (f+1);
break;
}
}
if ( i < Saig_ManPoNum(pAig) )
break;
}
Aig_ManCleanMarkB(pAig);
if ( f == nFrames )
{
Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Cannot find a failed primary outputs.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
if ( !Saig_ManVerifyCex( pAig, pCex ) )
{
Abc_Print( -1, "Saig_ManPbaDeriveCex(): Internal error! Counter-example is invalid.\n" );
Abc_CexFree( pCex );
pCex = NULL;
}
return pCex;
}
......@@ -199,7 +243,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 )
Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nInputs, int nFrames, int nConfLimit, int fVerbose, int * piFrame )
{
Vec_Int_t * vFlops = NULL, * vMapVar2FF, * vAssumps, * vPiVarMap;
Aig_Man_t * pFrames;
......@@ -248,46 +292,40 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
{
if ( RetValue == l_True )
{
printf( "Saig_ManPerformPba(): The eproblem is SAT. Abstraction refinement is still not enabled.\n" );
/*
Vec_Int_t * vAbsFfsToAdd;
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Saig_ManPbaDeriveCex( pAig, pSat, pCnf, nFrames, vPiVarMap );
printf( "The problem is SAT in frame %d. Performing CEX-based refinement.\n", pAig->pSeqModel->iFrame );
*piFrame = pAig->pSeqModel->iFrame;
// CEX is detected - refine the flops
vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAig, nInputs, pAig->pSeqModel, fVerbose );
if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
{
Vec_IntFree( vAbsFfsToAdd );
return NULL;
goto finish;
}
if ( fVerbose )
{
printf( "Adding %d registers to the abstraction. ", Vec_IntSize(vAbsFfsToAdd) );
Abc_PrintTime( 0, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", clock() - clk );
}
vFlops = vAbsFfsToAdd;
*/
}
else
{
printf( "Saig_ManPerformPba(): SAT solver timed out. Abstraction is not changed.\n" );
printf( "Saig_ManPerformPba(): SAT solver timed out. Current abstraction is not changed.\n" );
}
Vec_IntFree( vPiVarMap );
Vec_IntFree( vAssumps );
Vec_IntFree( vMapVar2FF );
sat_solver_delete( pSat );
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
return NULL;
goto finish;
}
assert( RetValue == l_False ); // UNSAT
*piFrame = nFrames;
// 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 );
printf( "AnalizeFinal after %d frames selected %d assumptions (out of %d). Conflicts = %d.\n",
nFrames, nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
// collect flops
vFlops = Vec_IntAlloc( nCoreLits );
......@@ -300,6 +338,7 @@ Abc_PrintTime( 1, "Solving", clock() - clk );
Vec_IntSort( vFlops, 0 );
// cleanup
finish:
Vec_IntFree( vPiVarMap );
Vec_IntFree( vAssumps );
Vec_IntFree( vMapVar2FF );
......
src/aig/saig/saigAbsStart.c
......@@ -196,7 +196,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) );
Abc_PrintTime( 0, "Time", clock() - clk );
Abc_PrintTime( 1, "Time", clock() - clk );
}
// vFlopsNew contains PI number that should be kept in pAbs
// add to the abstraction
......
src/aig/saig/saigBmc3.c
......@@ -1292,6 +1292,9 @@ clkOther += clock() - clk2;
fflush( stdout );
}
}
// consider the next timeframe
if ( RetValue == -1 && pPars->nStart == 0 )
pPars->iFrame = f;
//ABC_PRT( "CNF generation runtime", clkOther );
if ( pPars->fVerbose )
{
......
src/base/abci/abc.c
......@@ -881,6 +881,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
void For_ManFileExperiment();
// For_ManFileExperiment();
}
{
void Bdc_SpfdDecomposeTest();
Bdc_SpfdDecomposeTest();
}
/*
{
int i1, i2, i3, i4, i5, i6, N, Counter = 0;
......@@ -28437,6 +28441,7 @@ 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 iFrame = -1;
int c;
Extra_UtilGetoptReset();
......@@ -28490,8 +28495,10 @@ 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 );
// Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose, &iFrame );
if ( iFrame >= 0 )
pAbc->nFrames = iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
......@@ -28591,7 +28598,8 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars );
pAbc->nFrames = pPars->iFrame;
if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment