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 12:31:28 -08:00
parent 840f5d1ca8
commit 2732cbc1ee
2 changed files with 28 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -133,6 +133,17 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t *
Wlc_NtkCleanMarks( p );
Wlc_NtkForEachCo( p, pObj, i )
Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
Vec_IntClear(vFlops);
Wlc_NtkForEachCi( p, pObj, i ) {
if ( !Wlc_ObjIsPi(pObj) ) {
Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
pObj->Mark = 1;
}
}
Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
Wlc_NtkForEachObj( p, pObj, i )
@ -312,6 +323,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams( pPdrPars );
pPdrPars->fVerbose = pPars->fPdrVerbose;
pPdrPars->fVeryVerbose = 1;
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
@ -356,8 +368,15 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
pAig = Gia_ManToAigSimple( pGia );
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
if (vClauses)
IPdr_ManRestore(pPdr, vClauses);
if ( vClauses ) {
if ( Vec_VecSize( vClauses) == 1 ) {
Vec_VecFree( vClauses );
vClauses = NULL;
} else {
assert( Vec_VecSize( vClauses) >= 2 );
IPdr_ManRestore(pPdr, vClauses);
}
}
RetValue = IPdr_ManSolveInt( pPdr );
@ -441,11 +460,12 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
// set up parameters to run PDR
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams( pPdrPars );
pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
//pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
//pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
//pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
//pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
pPdrPars->fVerbose = pPars->fPdrVerbose;
pPdrPars->fVeryVerbose = 1;
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{

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

@ -147,6 +147,9 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses )
assert(vClauses);
printf( "IPdr restore:\n" );
IPdr_ManPrintClauses( vClauses, 0, Aig_ManRegNum( p->pAig ) );
Vec_VecFree(p->vClauses);
p->vClauses = vClauses;