Commit a8f6e5c6 by Yen-Sheng Ho

added an option -b to %pdra

parent a7bc919b
...@@ -174,6 +174,7 @@ struct Wlc_Par_t_ ...@@ -174,6 +174,7 @@ struct Wlc_Par_t_
int fPushClauses; // Push clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace
int fMFFC; // Refine the entire MFFC of a PPI int fMFFC; // Refine the entire MFFC of a PPI
int fPdra; // Use pdr -nct int fPdra; // Use pdr -nct
int fProofRefine; // Use proof-based refinement
int fVerbose; // verbose output int fVerbose; // verbose output
int fPdrVerbose; // verbose output int fPdrVerbose; // verbose output
}; };
...@@ -311,6 +312,7 @@ extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); ...@@ -311,6 +312,7 @@ extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ); extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops ); extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops );
extern Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p );
extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p ); extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis ); extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p ); extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p );
......
...@@ -49,7 +49,7 @@ int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) ...@@ -49,7 +49,7 @@ int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk )
return num; return num;
} }
static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, int sel_pi_first, int nConfLimit ) static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars )
{ {
Vec_Int_t * vCores = NULL; Vec_Int_t * vCores = NULL;
Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames );
...@@ -93,13 +93,13 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num ...@@ -93,13 +93,13 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num
Vec_IntPush(vLits, toLitCond(var, 0)); Vec_IntPush(vLits, toLitCond(var, 0));
} }
{ /*
int i, Entry; int i, Entry;
Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) ); Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) );
Vec_IntForEachEntry(vLits, Entry, i) Vec_IntForEachEntry(vLits, Entry, i)
Abc_Print( 1, "%d ", Entry); Abc_Print( 1, "%d ", Entry);
Abc_Print( 1, "\n", Entry); Abc_Print( 1, "\n");
} */
int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0)); int status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0));
if (status == l_False) { if (status == l_False) {
Abc_Print( 1, "UNSAT.\n" ); Abc_Print( 1, "UNSAT.\n" );
...@@ -167,7 +167,7 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i ...@@ -167,7 +167,7 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i
} }
else if (i >= nbits_old_pis + num_ppis + num_sel_pis) else if (i >= nbits_old_pis + num_ppis + num_sel_pis)
{ {
Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis); Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis - num_ppis);
} }
} }
Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i ) Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i )
...@@ -188,17 +188,19 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i ...@@ -188,17 +188,19 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, i
return pFrames; return pFrames;
} }
Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
{ {
if ( vNodes == NULL ) return NULL; if ( vBlacks== NULL ) return NULL;
Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
Wlc_Ntk_t * pNew; Wlc_Ntk_t * pNew;
Wlc_Obj_t * pObj; Wlc_Obj_t * pObj;
int i, k, iObj, iFanin; int i, k, iObj, iFanin;
Vec_Int_t * vFanins = Vec_IntAlloc( 3 ); Vec_Int_t * vFanins = Vec_IntAlloc( 3 );
Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNum(pNtk) ); Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
int nOrigObjNum = Wlc_NtkObjNumMax( pNtk ); int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
Wlc_Ntk_t * p = Wlc_NtkDupDfs( pNtk, 0, 1 ); Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
{ {
...@@ -218,10 +220,17 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) ...@@ -218,10 +220,17 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes )
Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) ); 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 )
{
iObj = Wlc_ObjId( p, pObj );
Vec_IntWriteEntry( vMapNode2Sel, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0 ) );
}
// iterate through the nodes in the DFS order // iterate through the nodes in the DFS order
Wlc_NtkForEachObj( p, pObj, i ) Wlc_NtkForEachObj( p, pObj, i )
{ {
int isSigned, range, iSelID; int isSigned, range;
if ( i == nOrigObjNum ) if ( i == nOrigObjNum )
{ {
// cout << "break at " << i << endl; // cout << "break at " << i << endl;
...@@ -234,9 +243,8 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) ...@@ -234,9 +243,8 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes )
isSigned = Wlc_ObjIsSigned(pObj); isSigned = Wlc_ObjIsSigned(pObj);
range = Wlc_ObjRange(pObj); range = Wlc_ObjRange(pObj);
iSelID = Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0);
Vec_IntClear(vFanins); Vec_IntClear(vFanins);
Vec_IntPush(vFanins, iSelID); Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) ); Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
Vec_IntPush(vFanins, i); Vec_IntPush(vFanins, i);
iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins); iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
...@@ -267,15 +275,127 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) ...@@ -267,15 +275,127 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes )
} }
// DumpWlcNtk(p); // DumpWlcNtk(p);
pNew = Wlc_NtkDupDfs( p, 0, 1 ); pNew = Wlc_NtkDupDfsSimple( p );
Vec_IntFree( vFanins ); Vec_IntFree( vFanins );
Vec_IntFree( vMapNode2Pi ); Vec_IntFree( vMapNode2Pi );
Vec_IntFree( vMapNode2Sel );
Vec_IntFree( vNodes );
Wlc_NtkFree( p ); Wlc_NtkFree( p );
return pNew; return pNew;
} }
static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops )
{
Vec_Int_t * vFlops = Vec_IntAlloc( 100 );
Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
Wlc_Ntk_t * pNew;
Wlc_Obj_t * pObj;
int i, k, iObj, iFanin;
Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
if ( vNodes == NULL )
return NULL;
Wlc_Ntk_t * p = NULL;
p = Wlc_NtkDupDfsSimple( pNtk );
Wlc_NtkForEachCi( pNtk, pObj, i )
{
if ( !Wlc_ObjIsPi( pObj ) )
Vec_IntPush( vFlops, Wlc_ObjId( pNtk, pObj ) );
}
Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
// mark nodes
Wlc_NtkForEachObjVec( vNodes, 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 ) );
}
Wlc_NtkCleanCopy( p );
Wlc_NtkForEachObj( p, pObj, i )
{
if ( i == nOrigObjNum )
break;
if ( pObj->Mark ) {
// clean
pObj->Mark = 0;
iObj = Vec_IntEntry( vMapNode2Pi, i );
}
else {
// update fanins
Wlc_ObjForEachFanin( pObj, iFanin, k )
Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
// node to remain
iObj = i;
}
Wlc_ObjSetCopy( p, i, iObj );
}
Wlc_NtkForEachCo( p, pObj, i )
{
iObj = Wlc_ObjId(p, pObj);
if (iObj != Wlc_ObjCopy(p, iObj))
{
if (pObj->fIsFi)
Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1;
else
Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1;
Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj));
}
}
pNew = Wlc_NtkDupDfsSimple( p );
Vec_IntFree( vMapNode2Pi );
Vec_IntFree( vNodes );
Wlc_NtkFree( p );
if ( pvFlops )
*pvFlops = vFlops;
else
Vec_IntFree( vFlops );
return pNew;
}
static Vec_Int_t * Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vBlacks )
{
Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
Wlc_Ntk_t * pNtkWithChoices = Wlc_NtkIntroduceChoices( p, vBlacks );
Vec_Int_t * vCoreSels;
int num_ppis = -1;
int Entry, i;
Gia_Man_t * pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 );
vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, 0, 0, pPars );
Vec_IntForEachEntry( vCoreSels, Entry, i )
Vec_IntPush( vRefine, Vec_IntEntry( vBlacks, Entry ) );
Wlc_NtkFree( pNtkWithChoices );
Gia_ManStop( pGiaFrames );
Vec_IntFree( vCoreSels );
if ( Vec_IntSize( vRefine ) == 0 )
{
Vec_IntFree( vRefine );
vRefine = NULL;
}
return vRefine;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Mark operators that meet the abstraction criteria.] Synopsis [Mark operators that meet the abstraction criteria.]
...@@ -289,6 +409,45 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes ) ...@@ -289,6 +409,45 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark )
{
Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ;
Wlc_Obj_t * pObj; int i, Count[4] = {0};
Wlc_NtkForEachObj( p, pObj, i )
{
if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
continue;
if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
continue;
}
if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
continue;
}
if ( pObj->Type == WLC_OBJ_MUX )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
continue;
}
if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[3]++;
continue;
}
}
if ( pPars->fVerbose )
printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
return vBlacks;
}
static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose ) static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
{ {
Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) ); Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
...@@ -641,7 +800,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -641,7 +800,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{ {
Aig_Man_t * pAig; Aig_Man_t * pAig;
Abc_Cex_t * pCex; Abc_Cex_t * pCex;
Vec_Int_t * vPisNew, * vRefine; Vec_Int_t * vPisNew = NULL;
Vec_Int_t * vRefine;
Gia_Man_t * pGia, * pTemp; Gia_Man_t * pGia, * pTemp;
Wlc_Ntk_t * pAbs; Wlc_Ntk_t * pAbs;
...@@ -649,7 +809,15 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -649,7 +809,15 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
printf( "\nIteration %d:\n", nIters ); printf( "\nIteration %d:\n", nIters );
// get abstracted GIA and the set of pseudo-PIs (vPisNew) // get abstracted GIA and the set of pseudo-PIs (vPisNew)
pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose ); if ( pPars->fProofRefine )
{
vPisNew = Wlc_NtkGetBlacks( p, pPars, vUnmark );
pAbs = Wlc_NtkAbs2( p, vPisNew, &vFfNew );
}
else
{
pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
}
pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 ); pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
// map old flops into new flops // map old flops into new flops
...@@ -720,7 +888,10 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -720,7 +888,10 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
} }
// perform refinement // perform refinement
vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); if ( pPars->fProofRefine )
vRefine = Wlc_NtkProofRefine( p, pPars, pGia, pCex, vPisNew );
else
vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
Gia_ManStop( pGia ); Gia_ManStop( pGia );
Vec_IntFree( vPisNew ); Vec_IntFree( vPisNew );
if ( vRefine == NULL ) // real CEX if ( vRefine == NULL ) // real CEX
...@@ -754,7 +925,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -754,7 +925,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Abc_CexFree( pCex ); Abc_CexFree( pCex );
Aig_ManStop( pAig ); Aig_ManStop( pAig );
} }
Vec_IntFreeP( &vFfOld ); Vec_IntFreeP( &vFfOld );
Vec_BitFree( vUnmark ); Vec_BitFree( vUnmark );
// report the result // report the result
......
...@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c; int c;
Wlc_ManSetDefaultParams( pPars ); Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIacpmxvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIabcpmxvwh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -524,6 +524,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -524,6 +524,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'a': case 'a':
pPars->fPdra ^= 1; pPars->fPdra ^= 1;
break; break;
case 'b':
pPars->fProofRefine ^= 1;
break;
case 'x': case 'x':
pPars->fXorOutput ^= 1; pPars->fXorOutput ^= 1;
break; break;
...@@ -556,7 +559,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -556,7 +559,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars ); Wlc_NtkPdrAbs( pNtk, pPars );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-acpmxvwh]\n" ); Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-abcpmxvwh]\n" );
Abc_Print( -2, "\t abstraction for word-level networks\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-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 ); Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
...@@ -564,7 +567,8 @@ usage: ...@@ -564,7 +567,8 @@ usage:
Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" ); Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" );
Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" );
Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "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-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" ); Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" );
......
...@@ -108,18 +108,19 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; } ...@@ -108,18 +108,19 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
{ {
memset( pPars, 0, sizeof(Wlc_Par_t) ); memset( pPars, 0, sizeof(Wlc_Par_t) );
pPars->nBitsAdd = ABC_INFINITY; // adder bit-width pPars->nBitsAdd = ABC_INFINITY; // adder bit-width
pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht
pPars->nBitsMux = ABC_INFINITY; // MUX bit-width pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
pPars->nBitsFlop = ABC_INFINITY; // flop bit-width pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
pPars->nIterMax = 1000; // the max number of iterations pPars->nIterMax = 1000; // the max number of iterations
pPars->fXorOutput = 1; // XOR outputs of word-level miter pPars->fXorOutput = 1; // XOR outputs of word-level miter
pPars->fCheckClauses = 1; // Check clauses in the reloaded trace pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
pPars->fPushClauses = 0; // Push clauses in the reloaded trace pPars->fPushClauses = 0; // Push clauses in the reloaded trace
pPars->fMFFC = 1; // Refine the entire MFFC of a PPI pPars->fMFFC = 1; // Refine the entire MFFC of a PPI
pPars->fPdra = 0; // Use pdr -nct pPars->fPdra = 0; // Use pdr -nct
pPars->fVerbose = 0; // verbose output` pPars->fProofRefine = 0; // Use proof-based refinement
pPars->fPdrVerbose = 0; // show verbose PDR output pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -832,6 +833,33 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v ...@@ -832,6 +833,33 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins ); Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
Wlc_ObjDup( pNew, p, iObj, vFanins ); Wlc_ObjDup( pNew, p, iObj, vFanins );
} }
Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p )
{
Wlc_Ntk_t * pNew;
Wlc_Obj_t * pObj;
Vec_Int_t * vFanins;
int i;
Wlc_NtkCleanCopy( p );
vFanins = Vec_IntAlloc( 100 );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
Wlc_NtkForEachCi( p, pObj, i )
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
Wlc_NtkForEachCo( p, pObj, i )
Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
Wlc_NtkForEachCo( p, pObj, i )
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
if ( p->vInits )
pNew->vInits = Vec_IntDup( p->vInits );
if ( p->pInits )
pNew->pInits = Abc_UtilStrsav( p->pInits );
Vec_IntFree( vFanins );
if ( p->pSpec )
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
return pNew;
}
Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ) Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
{ {
Wlc_Ntk_t * pNew; Wlc_Ntk_t * pNew;
......
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