summaryrefslogtreecommitdiffstats
path: root/src/base/wlc
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/wlc')
-rw-r--r--src/base/wlc/wlc.h10
-rw-r--r--src/base/wlc/wlcAbs.c710
-rw-r--r--src/base/wlc/wlcCom.c50
-rw-r--r--src/base/wlc/wlcNtk.c52
-rw-r--r--src/base/wlc/wlcStdin.c2
5 files changed, 795 insertions, 29 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 686d9f00..f5dbba42 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -169,9 +169,14 @@ struct Wlc_Par_t_
int nBitsMux; // MUX bit-width
int nBitsFlop; // flop bit-width
int nIterMax; // the max number of iterations
+ int nLimit; // the max number of signals
int fXorOutput; // XOR outputs of word-level miter
- int fCheckClauses; // Check clauses in the reloaded trace
- int fPushClauses; // Push clauses in the reloaded trace
+ int fCheckClauses; // Check clauses in the reloaded trace
+ int fPushClauses; // Push clauses in the reloaded trace
+ int fMFFC; // Refine the entire MFFC of a PPI
+ int fPdra; // Use pdr -nct
+ int fProofRefine; // Use proof-based refinement
+ int fHybrid; // Use a hybrid of CBR and PBR
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
@@ -309,6 +314,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 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_NtkDupDfsSimple( 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_NtkProfileCones( Wlc_Ntk_t * p );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index e33424f7..ad6c6642 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -34,10 +34,616 @@ extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
+typedef struct Int_Pair_t_ Int_Pair_t;
+struct Int_Pair_t_
+{
+ int first;
+ int second;
+};
+
+int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b )
+{
+ return (*a)->second < (*b)->second;
+}
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk )
+{
+ int num = 0;
+ int i;
+ Wlc_Obj_t * pObj;
+ Wlc_NtkForEachPi(pNtk, pObj, i) {
+ num += Wlc_ObjRange(pObj);
+ }
+ return num;
+}
+
+static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars )
+{
+ Vec_Int_t * vCores = NULL;
+ Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames );
+ Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames));
+ sat_solver * pSat = sat_solver_new();
+ int i;
+
+ sat_solver_setnvars(pSat, pCnf->nVars);
+
+ for (i = 0; i < pCnf->nClauses; i++)
+ {
+ if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1]))
+ assert(false);
+ }
+ // add PO clauses
+ {
+ Vec_Int_t* vLits = Vec_IntAlloc(100);
+ Aig_Obj_t* pObj;
+ int i, ret;
+ Aig_ManForEachCo( pAigFrames, pObj, i )
+ {
+ assert(pCnf->pVarNums[pObj->Id] >= 0);
+ Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0));
+ }
+ ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits));
+ if (!ret)
+ Abc_Print( 1, "UNSAT after adding PO clauses.\n" );
+
+ Vec_IntFree(vLits);
+ }
+ // main procedure
+ {
+ int status;
+ Vec_Int_t* vLits = Vec_IntAlloc(100);
+ Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars );
+ int first_sel_pi = sel_pi_first ? 0 : num_other_pis;
+ for ( i = 0; i < num_sel_pis; ++i )
+ {
+ int cur_pi = first_sel_pi + i;
+ int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id];
+ int Lit;
+ assert(var >= 0);
+ Vec_IntWriteEntry( vMapVar2Sel, var, i );
+ Lit = toLitCond( var, 0 );
+ if ( Vec_BitEntry( vMark, i ) )
+ Vec_IntPush(vLits, Lit);
+ else
+ sat_solver_addclause( pSat, &Lit, &Lit+1 );
+ }
+ /*
+ int i, Entry;
+ Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) );
+ Vec_IntForEachEntry(vLits, Entry, i)
+ Abc_Print( 1, "%d ", Entry);
+ Abc_Print( 1, "\n");
+ */
+ 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) {
+ int nCoreLits, *pCoreLits;
+ Abc_Print( 1, "UNSAT.\n" );
+ nCoreLits = sat_solver_final(pSat, &pCoreLits);
+ vCores = Vec_IntAlloc( nCoreLits );
+ for (i = 0; i < nCoreLits; i++)
+ {
+ Vec_IntPush( vCores, Vec_IntEntry( vMapVar2Sel, lit_var( pCoreLits[i] ) ) );
+ }
+ } else if (status == l_True) {
+ Abc_Print( 1, "SAT.\n" );
+ } else {
+ Abc_Print( 1, "UNKNOWN.\n" );
+ }
+
+ Vec_IntFree(vLits);
+ Vec_IntFree(vMapVar2Sel);
+ }
+ Cnf_ManFree();
+ sat_solver_delete(pSat);
+ Aig_ManStop(pAigFrames);
+
+ return vCores;
+}
+
+static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first)
+{
+ Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 );
+ int nbits_new_pis = Wlc_NtkNumPiBits( pChoice );
+ int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis;
+ int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis;
+ Gia_Man_t * pFrames = NULL;
+ Gia_Obj_t * pObj, * pObjRi;
+ int f, i;
+ int is_sel_pi;
+ Gia_Man_t * pGia;
+ *p_num_ppis = num_ppis;
+
+ Abc_Print( 1, "#orig_pis = %d, #ppis = %d, #sel_pis = %d, #undc_pis = %d\n", nbits_old_pis, num_ppis, num_sel_pis, num_undc_pis );
+ assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis);
+ assert(Gia_ManPiNum(pGiaChoice)==pCex->nPis+num_sel_pis);
+
+ pFrames = Gia_ManStart( 10000 );
+ pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName );
+ Gia_ManHashAlloc( pFrames );
+ Gia_ManConst0(pGiaChoice)->Value = 0;
+ Gia_ManForEachRi( pGiaChoice, pObj, i )
+ pObj->Value = 0;
+
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ {
+ for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ )
+ {
+ if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis )
+ {
+ is_sel_pi = sel_pi_first ? (i < nbits_old_pis + num_sel_pis) : (i >= nbits_old_pis + num_ppis);
+ if(f == 0 || !is_sel_pi)
+ Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+ }
+ else if (i < nbits_old_pis)
+ {
+ Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
+ }
+ 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 - num_ppis);
+ }
+ }
+ Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i )
+ pObj->Value = pObjRi->Value;
+ Gia_ManForEachAnd( pGiaChoice, pObj, i )
+ pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj));
+ Gia_ManForEachCo( pGiaChoice, pObj, i )
+ pObj->Value = Gia_ObjFanin0Copy(pObj);
+ Gia_ManForEachPo( pGiaChoice, pObj, i )
+ Gia_ManAppendCo(pFrames, pObj->Value);
+ }
+ Gia_ManHashStop (pFrames);
+ Gia_ManSetRegNum(pFrames, 0);
+ pFrames = Gia_ManCleanup(pGia = pFrames);
+ Gia_ManStop(pGia);
+ Gia_ManStop(pGiaChoice);
+
+ return pFrames;
+}
+
+Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
+{
+ //if ( vBlacks== NULL ) return NULL;
+ Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
+ Wlc_Ntk_t * pNew;
+ Wlc_Obj_t * pObj;
+ int i, k, iObj, iFanin;
+ Vec_Int_t * vFanins = Vec_IntAlloc( 3 );
+ Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+ Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+ int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
+ Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
+
+ Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
+ {
+ // TODO : fix FOs here
+ Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
+ }
+
+ // Vec_IntPrint(vNodes);
+ Wlc_NtkCleanCopy( p );
+
+ // 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 ) );
+ }
+
+ // 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
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ int isSigned, range;
+ if ( i == nOrigObjNum )
+ {
+ // cout << "break at " << i << endl;
+ break;
+ }
+ 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;
+ }
+ 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));
+ }
+ }
+
+ // DumpWlcNtk(p);
+ pNew = Wlc_NtkDupDfsSimple( p );
+
+ Vec_IntFree( vFanins );
+ Vec_IntFree( vMapNode2Pi );
+ Vec_IntFree( vMapNode2Sel );
+ Vec_IntFree( vNodes );
+ Wlc_NtkFree( p );
+
+ 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 );
+ Wlc_Ntk_t * 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 int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine )
+{
+ Gia_Man_t * pGiaFrames;
+ Vec_Int_t * vRefine = NULL;
+ Vec_Bit_t * vUnmark;
+ Vec_Bit_t * vChoiceMark;
+ Wlc_Ntk_t * pNtkWithChoices = NULL;
+ Vec_Int_t * vCoreSels;
+ int num_ppis = -1;
+ int Entry, i;
+
+ if ( *pvRefine == NULL )
+ return 0;
+
+ vUnmark = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
+ vChoiceMark = Vec_BitStart( Vec_IntSize( vBlacks ) );
+
+ Vec_IntForEachEntry( *pvRefine, Entry, i )
+ Vec_BitWriteEntry( vUnmark, Entry, 1 );
+
+ Vec_IntForEachEntry( vBlacks, Entry, i )
+ {
+ if ( Vec_BitEntry( vUnmark, Entry ) )
+ Vec_BitWriteEntry( vChoiceMark, i, 1 );
+ }
+
+ pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL;
+ 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, vChoiceMark, 0, 0, pPars );
+ Wlc_NtkFree( pNtkWithChoices );
+ Gia_ManStop( pGiaFrames );
+ Vec_BitFree( vUnmark );
+ Vec_BitFree( vChoiceMark );
+
+ assert( Vec_IntSize( vCoreSels ) );
+
+ vRefine = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntry( vCoreSels, Entry, i )
+ Vec_IntPush( vRefine, Vec_IntEntry( vBlacks, Entry ) );
+
+ Vec_IntFree( vCoreSels );
+
+ if ( pPars->fVerbose )
+ Abc_Print( 1, "Proof-based refinement reduces %d (out of %d) white boxes\n", Vec_IntSize( *pvRefine ) - Vec_IntSize( vRefine ), Vec_IntSize( *pvRefine ) );
+
+ Vec_IntFree( *pvRefine );
+ *pvRefine = vRefine;
+
+ return 0;
+}
+
+static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark )
+{
+ int Entry, i;
+ Wlc_Obj_t * pObj; int Count[4] = {0};
+ Vec_Int_t * vBlacks = Vec_IntAlloc( 100 );
+
+ assert( *pvBlacks );
+
+ Vec_IntForEachEntry( *pvBlacks, Entry, i )
+ {
+ if ( Vec_BitEntry( vUnmark, Entry) )
+ continue;
+ Vec_IntPush( vBlacks, Entry );
+
+ pObj = Wlc_NtkObj( p, Entry );
+ if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+ Count[0]++;
+ else 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 )
+ Count[1]++;
+ else if ( pObj->Type == WLC_OBJ_MUX )
+ Count[2]++;
+ else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+ Count[3]++;
+ }
+
+ Vec_IntFree( *pvBlacks );
+ *pvBlacks = vBlacks;
+
+ 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], Vec_IntSize( vBlacks ) - Count[0] - Count[1] - Count[2] );
+
+ return 0;
+}
+
+static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+ Vec_Bit_t * vMarks = NULL;
+ Vec_Ptr_t * vAdds = Vec_PtrAlloc( 1000 );
+ Vec_Ptr_t * vMuxes = Vec_PtrAlloc( 1000 );
+ Vec_Ptr_t * vMults = Vec_PtrAlloc( 1000 );
+ Vec_Ptr_t * vFlops = Vec_PtrAlloc( 1000 );
+ Wlc_Obj_t * pObj; int i;
+ Int_Pair_t * pPair;
+
+ if ( pPars->nLimit == ABC_INFINITY )
+ return NULL;
+
+ vMarks = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
+
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ 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 )
+ {
+ pPair = ABC_ALLOC( Int_Pair_t, 1 );
+ pPair->first = i;
+ pPair->second = Wlc_ObjRange( pObj );
+ Vec_PtrPush( vAdds, pPair );
+ }
+ }
+ else 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 )
+ {
+ pPair = ABC_ALLOC( Int_Pair_t, 1 );
+ pPair->first = i;
+ pPair->second = Wlc_ObjRange( pObj );
+ Vec_PtrPush( vMults, pPair );
+ }
+ }
+ else if ( pObj->Type == WLC_OBJ_MUX )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+ {
+ pPair = ABC_ALLOC( Int_Pair_t, 1 );
+ pPair->first = i;
+ pPair->second = Wlc_ObjRange( pObj );
+ Vec_PtrPush( vMuxes, pPair );
+ }
+ }
+ else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+ {
+ pPair = ABC_ALLOC( Int_Pair_t, 1 );
+ pPair->first = i;
+ pPair->second = Wlc_ObjRange( pObj );
+ Vec_PtrPush( vFlops, pPair );
+ }
+ }
+ }
+
+ Vec_PtrSort( vAdds, (int (*)(void))IntPairPtrCompare ) ;
+ Vec_PtrSort( vMults, (int (*)(void))IntPairPtrCompare ) ;
+ Vec_PtrSort( vMuxes, (int (*)(void))IntPairPtrCompare ) ;
+ Vec_PtrSort( vFlops, (int (*)(void))IntPairPtrCompare ) ;
+
+ Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i )
+ {
+ if ( i >= pPars->nLimit ) break;
+ Vec_BitWriteEntry( vMarks, pPair->first, 1 );
+ }
+ if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th ADD has width = %d\n", i, pPair->second );
+
+ Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i )
+ {
+ if ( i >= pPars->nLimit ) break;
+ Vec_BitWriteEntry( vMarks, pPair->first, 1 );
+ }
+ if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUL has width = %d\n", i, pPair->second );
+
+ Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i )
+ {
+ if ( i >= pPars->nLimit ) break;
+ Vec_BitWriteEntry( vMarks, pPair->first, 1 );
+ }
+ if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second );
+
+ Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i )
+ {
+ if ( i >= pPars->nLimit ) break;
+ Vec_BitWriteEntry( vMarks, pPair->first, 1 );
+ }
+ if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th FF has width = %d\n", i, pPair->second );
+
+
+ Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i ) ABC_FREE( pPair );
+ Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i ) ABC_FREE( pPair );
+ Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) ABC_FREE( pPair );
+ Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i ) ABC_FREE( pPair );
+ Vec_PtrFree( vAdds );
+ Vec_PtrFree( vMults );
+ Vec_PtrFree( vMuxes );
+ Vec_PtrFree( vFlops );
+
+ return vMarks;
+}
+
+static void Wlc_NtkSetUnmark( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark )
+{
+ int Entry, i;
+ Vec_Bit_t * vMarks = Wlc_NtkMarkLimit( p, pPars );
+
+ Vec_BitForEachEntry( vMarks, Entry, i )
+ Vec_BitWriteEntry( vUnmark, i, Entry^1 );
+
+ Vec_BitFree( vMarks );
+}
+
+static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+ Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ;
+ Wlc_Obj_t * pObj; int i, Count[4] = {0};
+ Vec_Bit_t * vMarks = NULL;
+
+ vMarks = Wlc_NtkMarkLimit( p, pPars ) ;
+
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ 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 )
+ {
+ if ( vMarks == NULL )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
+ else if ( Vec_BitEntry( vMarks, i ) )
+ Vec_IntPushUniqueOrder( 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 )
+ {
+ if ( vMarks == NULL )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
+ else if ( Vec_BitEntry( vMarks, i ) )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
+ }
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_MUX )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+ {
+ if ( vMarks == NULL )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
+ else if ( Vec_BitEntry( vMarks, i ) )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
+ }
+ continue;
+ }
+ if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+ {
+ if ( vMarks == NULL )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
+ else if ( Vec_BitEntry( vMarks, i ) )
+ Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
+ }
+ continue;
+ }
+ }
+ if ( vMarks )
+ Vec_BitFree( vMarks );
+ 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;
+}
+
/**Function*************************************************************
Synopsis [Mark operators that meet the abstraction criteria.]
@@ -51,6 +657,7 @@ extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu
SeeAlso []
***********************************************************************/
+
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) );
@@ -302,6 +909,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.]
@@ -365,10 +983,12 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF
int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
abctime clk = Abc_Clock();
- abctime pdrClk;
+ abctime clk2;
+ abctime tPdr = 0, tCbr = 0, tPbr = 0, tTotal = 0;
Pdr_Man_t * pPdr;
Vec_Vec_t * vClauses = NULL;
Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL;
+ Vec_Int_t * vBlacks = NULL;
int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1;
// start the bitmap to mark objects that cannot be abstracted because of refinement
// currently, this bitmap is empty because abstraction begins without refinement
@@ -379,12 +999,21 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
pPdrPars->fVerbose = pPars->fPdrVerbose;
pPdrPars->fVeryVerbose = 0;
+ if ( pPars->fPdra )
+ {
+ 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
+ }
+
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
Aig_Man_t * pAig;
Abc_Cex_t * pCex;
- Vec_Int_t * vPisNew, * vRefine;
+ Vec_Int_t * vPisNew = NULL;
+ Vec_Int_t * vRefine;
Gia_Man_t * pGia, * pTemp;
Wlc_Ntk_t * pAbs;
@@ -392,7 +1021,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
printf( "\nIteration %d:\n", nIters );
// get abstracted GIA and the set of pseudo-PIs (vPisNew)
- pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+ if ( pPars->fProofRefine )
+ {
+ if ( vBlacks == NULL )
+ vBlacks = Wlc_NtkGetBlacks( p, pPars );
+ else
+ Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
+ pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew );
+ vPisNew = Vec_IntDup( vBlacks );
+ }
+ else
+ {
+ if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
+ Wlc_NtkSetUnmark( p, pPars, vUnmark );
+
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+ }
pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
// map old flops into new flops
@@ -438,7 +1082,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
pAig = Gia_ManToAigSimple( pGia );
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
- pdrClk = Abc_Clock();
+ clk2 = Abc_Clock();
if ( vClauses ) {
assert( Vec_VecSize( vClauses) >= 2 );
@@ -447,7 +1091,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Vec_IntFreeP( &vMap );
RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
- pPdr->tTotal += Abc_Clock() - pdrClk;
+ pPdr->tTotal += Abc_Clock() - clk2;
+ tPdr += pPdr->tTotal;
pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
@@ -463,7 +1108,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
}
// perform refinement
- vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ if ( pPars->fHybrid || !pPars->fProofRefine )
+ {
+ clk2 = Abc_Clock();
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ tCbr += Abc_Clock() - clk2;
+ }
+ else // proof-based only
+ {
+ vRefine = Vec_IntDup( vPisNew );
+ }
+ if ( pPars->fProofRefine )
+ {
+ clk2 = Abc_Clock();
+ Wlc_NtkProofRefine( p, pPars, pCex, vPisNew, &vRefine );
+ tPbr += Abc_Clock() - clk2;
+ }
Gia_ManStop( pGia );
Vec_IntFree( vPisNew );
if ( vRefine == NULL ) // real CEX
@@ -480,14 +1140,29 @@ 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 );
+ clk2 = Abc_Clock();
+ 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) );
+
+ }
+ tCbr += Abc_Clock() - clk2;
+
Vec_IntFree( vRefine );
Abc_CexFree( pCex );
Aig_ManStop( pAig );
}
-
+
+ if ( vBlacks )
+ Vec_IntFree( vBlacks );
Vec_IntFreeP( &vFfOld );
Vec_BitFree( vUnmark );
// report the result
@@ -501,7 +1176,18 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
else
printf( "timed out" );
printf( " after %d iterations. ", nIters );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ tTotal = Abc_Clock() - clk;
+ Abc_PrintTime( 1, "Time", tTotal );
+
+ if ( pPars->fVerbose )
+ {
+ ABC_PRTP( "PDR ", tPdr, tTotal );
+ ABC_PRTP( "CEX Refine ", tCbr, tTotal );
+ ABC_PRTP( "Proof Refine ", tPbr, tTotal );
+ ABC_PRTP( "Misc. ", tTotal - tPdr - tCbr - tPbr, tTotal );
+ ABC_PRTP( "Total ", tTotal, tTotal );
+ }
+
return RetValue;
}
@@ -550,6 +1236,8 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
printf( "\nIteration %d:\n", nIters );
// get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
+ Wlc_NtkSetUnmark( p, pPars, vUnmark );
pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index df736e70..38f919d4 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -521,6 +521,26 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nIterMax < 0 )
goto usage;
break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLimit < 0 )
+ goto usage;
+ break;
+ case 'a':
+ pPars->fPdra ^= 1;
+ break;
+ case 'b':
+ pPars->fProofRefine ^= 1;
+ break;
+ case 'r':
+ pPars->fHybrid ^= 1;
+ break;
case 'x':
pPars->fXorOutput ^= 1;
break;
@@ -530,6 +550,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
pPars->fPushClauses ^= 1;
break;
+ case 'm':
+ pPars->fMFFC ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -550,16 +573,21 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
- Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
+ Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\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-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
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-L num : maximum number of each type of signals [default = %d]\n", pPars->nLimit );
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-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" );
+ Abc_Print( -2, "\t-r : toggle using both cex-based and proof-based refinement [default = %s]\n", pPars->fHybrid? "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-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -585,7 +613,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -644,6 +672,17 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nIterMax < 0 )
goto usage;
break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLimit < 0 )
+ goto usage;
+ break;
case 'x':
pPars->fXorOutput ^= 1;
break;
@@ -667,13 +706,14 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkAbsCore( pNtk, pPars );
return 0;
usage:
- Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" );
+ Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-xvwh]\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-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
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-L num : maximum number of each type of signals [default = %d]\n", pPars->nLimit );
Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index c8fc15a7..89699949 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -108,16 +108,21 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
{
memset( pPars, 0, sizeof(Wlc_Par_t) );
- pPars->nBitsAdd = ABC_INFINITY; // adder bit-width
- pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht
- pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
- pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
- pPars->nIterMax = 1000; // the max number of iterations
- pPars->fXorOutput = 1; // XOR outputs of word-level miter
- pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
- pPars->fPushClauses = 0; // Push clauses in the reloaded trace
- pPars->fVerbose = 0; // verbose output`
- pPars->fPdrVerbose = 0; // show verbose PDR output
+ pPars->nBitsAdd = ABC_INFINITY; // adder bit-width
+ pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht
+ pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
+ pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
+ pPars->nIterMax = 1000; // the max number of iterations
+ pPars->nLimit = ABC_INFINITY; // the max number of signals
+ pPars->fXorOutput = 1; // XOR outputs of word-level miter
+ pPars->fCheckClauses = 1; // Check 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->fPdra = 0; // Use pdr -nct
+ pPars->fProofRefine = 0; // Use proof-based refinement
+ pPars->fHybrid = 1; // Use a hybrid of CBR and PBR
+ pPars->fVerbose = 0; // verbose output`
+ pPars->fPdrVerbose = 0; // show verbose PDR output
}
/**Function*************************************************************
@@ -830,6 +835,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_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 * pNew;
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index 49c25ad0..3b747cc5 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -239,7 +239,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
return 0;
}
// report value of this variable
- Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 );
+ Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 );
Vec_StrFree( vInput );
fflush( stdout );
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-23 18:56:35 +0000