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

%pdra: added an option -s

This commit is contained in:
Yen-Sheng Ho 2017-03-28 14:08:04 -07:00
parent 7a423e4fbe
commit 2fea987ec6
5 changed files with 86 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/wlc/wlc.h
View File

@ -181,6 +181,7 @@ struct Wlc_Par_t_
int fAbs2; // Use UFAR style createAbs
int fProofUsePPI; // Use PPI values in PBR
int fUseBmc3; // Run BMC3 in parallel
int fShrinkAbs; // Shrink Abs with BMC
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
@ -199,6 +200,9 @@ struct Wla_Man_t_
void * pPdrPars;
void * pThread;
int iCexFrame;
int fNewAbs;
int nIters;
int nTotalCla;
int nDisj;

68
src/base/wlc/wlcAbs.c
View File

@ -619,12 +619,11 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t
return pNew;
}
static Vec_Int_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFrames, Vec_Int_t * vWhites )
static Vec_Bit_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFrames, Vec_Int_t * vWhites )
{
Gia_Man_t * pGiaFrames;
Wlc_Ntk_t * pNtkWithChoices = NULL;
Vec_Int_t * vCoreSels;
Vec_Int_t * vCoreWhites = NULL;
Vec_Bit_t * vChoiceMark;
int first_sel_pi;
int i, Entry;
@ -642,16 +641,15 @@ static Vec_Int_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFr
Wlc_NtkFree( pNtkWithChoices );
Gia_ManStop( pGiaFrames );
Vec_BitFree( vChoiceMark );
vCoreWhites = Vec_IntAlloc( Vec_IntSize(vWhites) );
Vec_BitReset( vChoiceMark );
Vec_IntForEachEntry( vCoreSels, Entry, i )
Vec_IntPush( vCoreWhites, Vec_IntEntry( vWhites, Entry ) );
Vec_BitWriteEntry( vChoiceMark, Entry, 1 );
Abc_Print( 1, "ProofReduce: remove %d out of %d white boxes.\n", Vec_IntSize(vWhites) - Vec_IntSize(vCoreWhites), Vec_IntSize(vWhites) );
Abc_Print( 1, "ProofReduce: remove %d out of %d white boxes.\n", Vec_IntSize(vWhites) - Vec_BitCount(vChoiceMark), Vec_IntSize(vWhites) );
Vec_IntFree( vCoreSels );
return vCoreWhites;
return vChoiceMark;
}
static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine )
@ -1280,6 +1278,26 @@ Vec_Int_t * Wla_ManCollectWhites( Wla_Man_t * pWla )
return vWhites;
}
int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames )
{
int i, Entry;
int RetValue = 0;
Vec_Int_t * vWhites = Wla_ManCollectWhites( pWla );
Vec_Bit_t * vCoreMarks = Wlc_NtkProofReduce( pWla->p, pWla->pPars, nFrames, vWhites );
RetValue = Vec_IntSize( vWhites ) != Vec_BitCount( vCoreMarks );
Vec_IntForEachEntry( vWhites, Entry, i )
if ( !Vec_BitEntry( vCoreMarks, i ) )
Vec_BitWriteEntry( pWla->vUnmark, Entry, 0 );
Vec_IntFree( vWhites );
Vec_BitFree( vCoreMarks );
return RetValue;
}
Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
{
Wlc_Ntk_t * pAbs;
@ -1287,8 +1305,8 @@ Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
// get abstracted GIA and the set of pseudo-PIs (vBlacks)
if ( pWla->vBlacks == NULL )
{
pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars );
pWla->vSignals = Vec_IntDup( pWla->vBlacks );
pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars );
pWla->vSignals = Vec_IntDup( pWla->vBlacks );
}
else
{
@ -1421,8 +1439,13 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
if ( pWla->vClauses ) {
assert( Vec_VecSize( pWla->vClauses) >= 2 );
IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
//IPdr_ManRebuildClauses( pPdr, pWla->vClauses );
if ( pWla->fNewAbs )
IPdr_ManRebuildClauses( pPdr, pWla->vClauses );
else
IPdr_ManRestoreClauses( pPdr, pWla->vClauses, NULL );
pWla->fNewAbs = 0;
}
RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses );
@ -1464,6 +1487,14 @@ void Wla_ManRefine( Wla_Man_t * pWla )
abctime clk;
int nNodes;
Vec_Int_t * vRefine = NULL;
if ( pWla->fNewAbs )
{
assert( pWla->pCex == NULL );
Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
return;
}
// perform refinement
if ( pWla->pPars->fHybrid || !pWla->pPars->fProofRefine )
{
@ -1519,12 +1550,14 @@ void Wla_ManRefine( Wla_Man_t * pWla )
if ( pWla->pCex->iFrame > 0 )
{
Vec_Int_t * vWhites = Wla_ManCollectWhites( pWla );
Vec_Int_t * vCore = Wlc_NtkProofReduce( pWla->p, pWla->pPars, pWla->pCex->iFrame, vWhites );
Vec_Bit_t * vCore = Wlc_NtkProofReduce( pWla->p, pWla->pPars, pWla->pCex->iFrame, vWhites );
Vec_IntFree( vWhites );
Vec_IntFree( vCore );
Vec_BitFree( vCore );
}
*/
pWla->iCexFrame = pWla->pCex->iFrame;
Vec_IntFree( vRefine );
Gia_ManStop( pWla->pGia ); pWla->pGia = NULL;
Abc_CexFree( pWla->pCex ); pWla->pCex = NULL;
@ -1551,10 +1584,13 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars )
}
p->pPdrPars = (void *)pPdrPars;
p->nIters = 1;
p->iCexFrame = 0;
p->fNewAbs = 0;
p->nIters = 1;
p->nTotalCla = 0;
p->nDisj = 0;
p->nNDisj = 0;
p->nDisj = 0;
p->nNDisj = 0;
return p;
}

8
src/base/wlc/wlcCom.c
View File

@ -464,7 +464,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmuxvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipqmsuxvwh" ) ) != EOF )
{
switch ( c )
{
@ -564,6 +564,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
pPars->fMFFC ^= 1;
break;
case 's':
pPars->fShrinkAbs ^= 1;
break;
case 'u':
pPars->fCheckCombUnsat ^= 1;
break;
@ -587,7 +590,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxuvwh]\n" );
Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipqmxsuvwh]\n" );
Abc_Print( -2, "\t abstraction for word-level networks\n" );
Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
@ -602,6 +605,7 @@ usage:
Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
Abc_Print( -2, "\t-d : toggle using another way of creating abstractions [default = %s]\n", pPars->fAbs2? "yes": "no" );
Abc_Print( -2, "\t-i : toggle using PPI values in proof-based refinement [default = %s]\n", pPars->fProofUsePPI? "yes": "no" );
Abc_Print( -2, "\t-s : toggle shrinking abstractions with BMC [default = %s]\n", pPars->fShrinkAbs? "yes": "no" );
Abc_Print( -2, "\t-u : toggle checking combinationally unsat [default = %s]\n", pPars->fCheckCombUnsat? "yes": "no" );
Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
Abc_Print( -2, "\t-q : toggle running bmc3 in parallel for CEX [default = %s]\n", pPars->fUseBmc3? "yes": "no" );

1
src/base/wlc/wlcNtk.c
View File

@ -125,6 +125,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fAbs2 = 0; // Use UFAR style createAbs
pPars->fProofUsePPI = 0; // Use PPI values in PBR
pPars->fUseBmc3 = 0; // Run BMC3 in parallel
pPars->fShrinkAbs = 0; // Shrink Abs with BMC
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}

25
src/base/wlc/wlcPth.c
View File

@ -40,6 +40,7 @@ ABC_NAMESPACE_IMPL_START
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pAig );
extern int Abc_NtkDarBmc3( Abc_Ntk_t * pAbcNtk, Saig_ParBmc_t * pBmcPars, int fOrDecomp );
extern int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames );
static volatile int g_nRunIds = 0; // the number of the last prover instance
int Wla_CallBackToStop( int RunId ) { assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }
@ -55,6 +56,7 @@ void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppC
// information given to the thread
typedef struct Bmc3_ThData_t_
{
Wla_Man_t * pWla;
Aig_Man_t * pAig;
Abc_Cex_t ** ppCex;
int RunId;
@ -84,6 +86,7 @@ void * Wla_Bmc3Thread ( void * pArg )
{
int status;
int RetValue = -1;
int nFramesNoChangeLim = 10;
Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
@ -91,6 +94,9 @@ void * Wla_Bmc3Thread ( void * pArg )
pBmcPars->pFuncStop = Wla_CallBackToStop;
pBmcPars->RunId = pData->RunId;
if ( pData->pWla->nIters > 1 && pData->pWla->pPars->fShrinkAbs )
pBmcPars->nFramesMax = pData->pWla->iCexFrame + nFramesNoChangeLim;
RetValue = Abc_NtkDarBmc3( pAbcNtk, pBmcPars, 0 );
if ( RetValue == 0 )
@ -106,10 +112,24 @@ void * Wla_Bmc3Thread ( void * pArg )
++g_nRunIds;
status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
}
else
else if ( RetValue == -1 )
{
if ( pData->fVerbose )
if ( pData->RunId < g_nRunIds && pData->fVerbose )
Abc_Print( 1, "Bmc3 was cancelled. RunId=%d.\n", pData->RunId );
if ( pData->RunId == g_nRunIds )
{
RetValue = Wla_ManShrinkAbs( pData->pWla, pData->pWla->iCexFrame + nFramesNoChangeLim );
pData->pWla->iCexFrame += nFramesNoChangeLim;
if ( RetValue )
{
pData->pWla->fNewAbs = 1;
status = pthread_mutex_lock(&g_mutex); assert( status == 0 );
++g_nRunIds;
status = pthread_mutex_unlock(&g_mutex); assert( status == 0 );
}
}
}
// free memory
@ -132,6 +152,7 @@ void Wla_ManConcurrentBmc3( Wla_Man_t * pWla, Aig_Man_t * pAig, Abc_Cex_t ** ppC
pWla->pThread = (void *)ABC_CALLOC( pthread_t, 1 );
pData = ABC_CALLOC( Bmc3_ThData_t, 1 );
pData->pWla = pWla;
pData->pAig = pAig;
pData->ppCex = ppCex;
pData->RunId = g_nRunIds;