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

working on %pdra -m

This commit is contained in:
Yen-Sheng Ho 2017-02-22 17:57:19 -08:00
parent 2f90e5e15d
commit f01c63f712
1 changed files with 24 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -302,6 +302,17 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
return nNodes;
}
static int Wlc_NtkUnmarkRefinement( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
{
Wlc_Obj_t * pObj; int i, nNodes = 0;
Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
{
Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pObj), 1 );
++nNodes;
}
return nNodes;
}
/**Function*************************************************************
Synopsis [Computes the map for remapping flop IDs used in the clauses.]
@ -480,9 +491,19 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Pdr_ManStop( pPdr );
// 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 );
if ( pPars->fMFFC )
{
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 );
}
else
{
nNodes = Wlc_NtkUnmarkRefinement( p, vRefine, vUnmark );
if ( pPars->fVerbose )
printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) );
}
Vec_IntFree( vRefine );
Abc_CexFree( pCex );
Aig_ManStop( pAig );