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

working on pdr with wla

This commit is contained in:
Yen-Sheng Ho 2017-02-19 09:55:58 -08:00
parent 24fdcecb2d
commit 6cf289dadd
4 changed files with 120 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -277,6 +277,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
/*=== wlcAbs.c ========================================================*/
extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcAbs2.c ========================================================*/
extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcBlast.c ========================================================*/

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

@ -283,6 +283,117 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
return nNodes;
}
/**Function*************************************************************
Synopsis [Performs PDR with word-level abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
abctime clk = Abc_Clock();
int nIters, nNodes, nDcFlops, RetValue = -1;
// start the bitmap to mark objects that cannot be abstracted because of refinement
// currently, this bitmap is empty because abstraction begins without refinement
Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
// set up parameters to run PDR
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams( pPdrPars );
pPdrPars->fVerbose = pPars->fPdrVerbose;
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
Aig_Man_t * pAig;
Abc_Cex_t * pCex;
Vec_Int_t * vPisNew, * vRefine;
Gia_Man_t * pGia, * pTemp;
Wlc_Ntk_t * pAbs;
if ( pPars->fVerbose )
printf( "\nIteration %d:\n", nIters );
// get abstracted GIA and the set of pseudo-PIs (vPisNew)
pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
// if the abstraction has flops with DC-init state,
// new PIs were introduced by bit-blasting at the end of the PI list
// here we move these variables to be *before* PPIs, because
// PPIs are supposed to be at the end of the PI list for refinement
nDcFlops = Wlc_NtkDcFlopNum(pAbs);
if ( nDcFlops > 0 ) // DC-init flops are present
{
pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
Gia_ManStop( pTemp );
}
// if the word-level outputs have to be XORs, this is a place to do it
if ( pPars->fXorOutput )
{
pGia = Gia_ManTransformMiter2( pTemp = pGia );
Gia_ManStop( pTemp );
}
if ( pPars->fVerbose )
{
printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
Gia_ManPrintStats( pGia, NULL );
}
Wlc_NtkFree( pAbs );
// try to prove abstracted GIA by converting it to AIG and calling PDR
pAig = Gia_ManToAigSimple( pGia );
RetValue = Pdr_ManSolve( pAig, pPdrPars );
pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
// consider outcomes
if ( pCex == NULL )
{
assert( RetValue ); // proved or undecided
Gia_ManStop( pGia );
Vec_IntFree( vPisNew );
break;
}
// perform refinement
vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
Gia_ManStop( pGia );
Vec_IntFree( vPisNew );
if ( vRefine == NULL ) // real CEX
{
Abc_CexFree( pCex ); // return CEX in the future
break;
}
// update the set of objects to be un-abstracted
nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
if ( pPars->fVerbose )
printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
Vec_IntFree( vRefine );
Abc_CexFree( pCex );
}
Vec_BitFree( vUnmark );
// report the result
if ( pPars->fVerbose )
printf( "\n" );
printf( "Abstraction " );
if ( RetValue == 0 )
printf( "resulted in a real CEX" );
else if ( RetValue == 1 )
printf( "is successfully proved" );
else
printf( "timed out" );
printf( " after %d iterations. ", nIters );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs abstraction.]

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

@ -541,7 +541,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
return 0;
}
Wlc_NtkAbsCore( pNtk, pPars );
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" );

11
src/proof/pdr/pdrIncr.c
View File

@ -77,14 +77,17 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
SeeAlso []
***********************************************************************/
Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p )
Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
{
int i, k;
Vec_Vec_t * vClausesSaved;
Pdr_Set_t * pCla;
// Note that the last frame is empty
vClausesSaved = Vec_VecStart(Vec_VecSize(p->vClauses)-1);
if ( fDropLast )
vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 );
else
vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) );
Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) )
Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla));
@ -555,7 +558,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
RetValue = IPdr_ManSolveInt( p );
if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) {
vClausesSaved = IPdr_ManSaveClauses( p );
vClausesSaved = IPdr_ManSaveClauses( p, 1 );
Pdr_ManStop( p );