Skip to content

A
abc
Commit 4d479048 by Yen-Sheng Ho
Options

%pdra: fixed bugs

parent bf4be3fc
Showing with 78 additions and 39 deletions
src/base/wlc/wlcAbs.c
......@@ -427,7 +427,7 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i
return pFrames;
}
Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t * vPPIs )
{
//if ( vBlacks== NULL ) return NULL;
Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
......@@ -439,6 +439,7 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
Vec_Bit_t * vPPIMark = NULL;
Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
{
......@@ -446,6 +447,16 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
}
if ( vPPIs )
{
vPPIMark = Vec_BitStart( Wlc_NtkObjNumMax(pNtk) );
Wlc_NtkForEachObjVec( vPPIs, pNtk, pObj, i )
{
Vec_IntWriteEntry(vPPIs, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
Vec_BitWriteEntry( vPPIMark, Vec_IntEntry(vPPIs, i), 1 );
}
}
// Vec_IntPrint(vNodes);
Wlc_NtkCleanCopy( p );
......@@ -458,6 +469,17 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
}
if ( vPPIs )
{
Wlc_NtkForEachObjVec( vPPIs, p, pObj, i )
{
iObj = Wlc_ObjId(p, pObj);
pObj->Mark = 1;
// add fresh PI with the same number of bits
Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
}
}
// add sel PI
Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
{
......@@ -474,27 +496,32 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
// cout << "break at " << i << endl;
break;
}
// update fanins
Wlc_ObjForEachFanin( pObj, iFanin, k )
Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
// node to remain
iObj = i;
if ( pObj->Mark )
{
// clean
pObj->Mark = 0;
isSigned = Wlc_ObjIsSigned(pObj);
range = Wlc_ObjRange(pObj);
Vec_IntClear(vFanins);
Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
Vec_IntPush(vFanins, i);
iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
}
else
{
// update fanins
Wlc_ObjForEachFanin( pObj, iFanin, k )
Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
// node to remain
iObj = i;
if ( vPPIMark && Vec_BitEntry(vPPIMark, i) )
iObj = Vec_IntEntry( vMapNode2Pi, i );
else
{
isSigned = Wlc_ObjIsSigned(pObj);
range = Wlc_ObjRange(pObj);
Vec_IntClear(vFanins);
Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
Vec_IntPush(vFanins, i);
iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
}
}
Wlc_ObjSetCopy( p, i, iObj );
}
......@@ -515,6 +542,8 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
// DumpWlcNtk(p);
pNew = Wlc_NtkDupDfsSimple( p );
if ( vPPIMark )
Vec_BitFree( vPPIMark );
Vec_IntFree( vFanins );
Vec_IntFree( vMapNode2Pi );
Vec_IntFree( vMapNode2Sel );
......@@ -637,7 +666,7 @@ static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t
return pNew;
}
static Vec_Bit_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, Vec_Int_t * vBlacks )
{
Gia_Man_t * pGiaFrames;
Wlc_Ntk_t * pNtkWithChoices = NULL;
......@@ -648,15 +677,13 @@ static Vec_Bit_t * Wlc_NtkProofReduce( Wlc_Ntk_t * p, Wlc_Par_t * pPars, int nFr
abctime clk = Abc_Clock();
assert( vWhites && Vec_IntSize(vWhites) );
pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vWhites );
pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vWhites, vBlacks );
first_sel_pi = Wlc_NtkNumPiBits( pNtkWithChoices ) - Vec_IntSize( vWhites );
pGiaFrames = Wlc_NtkUnrollWoCex( pNtkWithChoices, nFrames, first_sel_pi, Vec_IntSize( vWhites ) );
vChoiceMark = Vec_BitStart( Vec_IntSize( vWhites ) );
Vec_IntForEachEntry( vWhites, Entry, i )
Vec_BitWriteEntry( vChoiceMark, i, 1 );
vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, nFrames, first_sel_pi, Vec_IntSize( vWhites ), vChoiceMark, 0, pPars, 1 );
vChoiceMark = Vec_BitStartFull( Vec_IntSize( vWhites ) );
vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, nFrames, first_sel_pi, Vec_IntSize( vWhites ), vChoiceMark, 0, pPars, 0 );
Wlc_NtkFree( pNtkWithChoices );
Gia_ManStop( pGiaFrames );
......@@ -698,7 +725,7 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe
Vec_BitWriteEntry( vChoiceMark, i, 1 );
}
pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL;
pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks, NULL ) : NULL;
pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0, pPars->fProofUsePPI );
if ( !pPars->fProofUsePPI )
......@@ -728,15 +755,18 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe
return 0;
}
static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark )
static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark, Vec_Int_t * vSignals )
{
int Entry, i;
Wlc_Obj_t * pObj; int Count[4] = {0};
Vec_Int_t * vBlacks = Vec_IntAlloc( 100 );
Vec_Int_t * vVec;
assert( *pvBlacks );
Vec_IntForEachEntry( *pvBlacks, Entry, i )
vVec = vSignals ? vSignals : *pvBlacks;
Vec_IntForEachEntry( vVec, Entry, i )
{
if ( Vec_BitEntry( vUnmark, Entry) )
continue;
......@@ -1281,21 +1311,24 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF
SeeAlso []
***********************************************************************/
Vec_Int_t * Wla_ManCollectWhites( Wla_Man_t * pWla )
Vec_Int_t * Wla_ManCollectNodes( Wla_Man_t * pWla, int fBlack )
{
Vec_Int_t * vWhites = NULL;
Vec_Int_t * vNodes = NULL;
int i, Entry;
assert( pWla->vSignals );
vWhites = Vec_IntAlloc( 100 );
vNodes = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( pWla->vSignals, Entry, i )
if ( Vec_BitEntry(pWla->vUnmark, Entry) )
Vec_IntPush( vWhites, Entry );
assert( Vec_IntSize(vWhites) );
{
if ( !fBlack && Vec_BitEntry(pWla->vUnmark, Entry) )
Vec_IntPush( vNodes, Entry );
if ( fBlack && !Vec_BitEntry(pWla->vUnmark, Entry) )
Vec_IntPush( vNodes, Entry );
}
return vWhites;
return vNodes;
}
int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames )
......@@ -1303,8 +1336,9 @@ 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 );
Vec_Int_t * vWhites = Wla_ManCollectNodes( pWla, 0 );
Vec_Int_t * vBlacks = Wla_ManCollectNodes( pWla, 1 );
Vec_Bit_t * vCoreMarks = Wlc_NtkProofReduce( pWla->p, pWla->pPars, nFrames, vWhites, vBlacks );
RetValue = Vec_IntSize( vWhites ) != Vec_BitCount( vCoreMarks );
......@@ -1313,6 +1347,7 @@ int Wla_ManShrinkAbs( Wla_Man_t * pWla, int nFrames )
Vec_BitWriteEntry( pWla->vUnmark, Entry, 0 );
Vec_IntFree( vWhites );
Vec_IntFree( vBlacks );
Vec_BitFree( vCoreMarks );
return RetValue;
......@@ -1330,7 +1365,7 @@ Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla )
}
else
{
Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark );
Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark, pWla->vSignals );
}
pAbs = Wlc_NtkAbs2( pWla->p, pWla->vBlacks, NULL );
......@@ -1739,7 +1774,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
if ( vBlacks == NULL )
vBlacks = Wlc_NtkGetBlacks( p, pPars );
else
Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark, NULL );
pAbs = Wlc_NtkAbs2( p, vBlacks, NULL );
vPisNew = Vec_IntDup( vBlacks );
}
......
src/base/wlc/wlcPth.c
......@@ -86,7 +86,7 @@ void * Wla_Bmc3Thread ( void * pArg )
{
int status;
int RetValue = -1;
int nFramesNoChangeLim = 10;
int nFramesNoChangeLim = 3;
Bmc3_ThData_t * pData = (Bmc3_ThData_t *)pArg;
Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase( pData->pAig );
Saig_ParBmc_t BmcPars, *pBmcPars = &BmcPars;
......
src/proof/pdr/pdrIncr.c
......@@ -272,7 +272,9 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
{
++nCubes;
RetValue = Pdr_ManCheckCube( p, 0, pCube, NULL, 0, 0, 1 );
Vec_IntWriteEntry( p->vActVars, 0, 0 );
assert( RetValue != -1 );
......@@ -288,7 +290,9 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
}
Abc_Print( 1, "RebuildClauses: %d out of %d cubes reused in R1.\n", Vec_PtrSize(Vec_VecEntry(p->vClauses, 1)), nCubes );
IPdr_ManSetSolver( p, 1, 0 );
Vec_VecFree( vClauses );
/*
for ( i = 1; i < Vec_VecSize( vClauses ) - 1; ++i )
{
vArrayK = IPdr_ManPushClausesK( p, i );
......@@ -308,8 +312,8 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
Vec_VecForEachLevel( p->vClauses, vArrayK, i )
Abc_Print( 1, " %d", Vec_PtrSize( vArrayK ) );
Abc_Print( 1, "\n" );
*/
Vec_VecFree( vClauses );
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