summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/wlc/wlc.h2
-rw-r--r--src/base/wlc/wlcAbs.c60
-rw-r--r--src/base/wlc/wlcCom.c20
-rw-r--r--src/base/wlc/wlcNtk.c2
4 files changed, 71 insertions, 13 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 699d2d9b..e1ec0d06 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -178,6 +178,8 @@ struct Wlc_Par_t_
int fProofRefine; // Use proof-based refinement
int fHybrid; // Use a hybrid of CBR and PBR
int fCheckCombUnsat; // Check if ABS becomes comb. unsat
+ int fAbs2; // Use UFAR style createAbs
+ int fProofUsePPI; // Use PPI values in PBR
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 79da6235..ca1d14a9 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -148,7 +148,7 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num
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)
+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, int fUsePPI)
{
Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 );
int nbits_new_pis = Wlc_NtkNumPiBits( pChoice );
@@ -179,8 +179,15 @@ static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, 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)
+ if( f == 0 && is_sel_pi )
Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+ if( !is_sel_pi )
+ {
+ if ( !fUsePPI )
+ Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+ else
+ Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i + num_undc_pis);
+ }
}
else if (i < nbits_old_pis)
{
@@ -446,8 +453,13 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe
}
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 );
+ pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0, pPars->fProofUsePPI );
+
+ if ( !pPars->fProofUsePPI )
+ vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars );
+ else
+ vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), 0, vChoiceMark, 0, 0, pPars );
+
Wlc_NtkFree( pNtkWithChoices );
Gia_ManStop( pGiaFrames );
Vec_BitFree( vUnmark );
@@ -625,6 +637,7 @@ 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;
+ int nTotal = 0;
vMarks = Wlc_NtkMarkLimit( p, pPars ) ;
@@ -634,6 +647,7 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
{
+ ++nTotal;
if ( vMarks == NULL )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
else if ( Vec_BitEntry( vMarks, i ) )
@@ -645,6 +659,7 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
{
+ ++nTotal;
if ( vMarks == NULL )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
else if ( Vec_BitEntry( vMarks, i ) )
@@ -656,6 +671,7 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
{
+ ++nTotal;
if ( vMarks == NULL )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
else if ( Vec_BitEntry( vMarks, i ) )
@@ -667,6 +683,7 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
{
+ ++nTotal;
if ( vMarks == NULL )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
else if ( Vec_BitEntry( vMarks, i ) )
@@ -678,7 +695,7 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
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] );
+ printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away (out of %d signals).\n", Count[0], Count[1], Count[2], Count[3], nTotal );
return vBlacks;
}
@@ -1028,6 +1045,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL;
Vec_Int_t * vBlacks = NULL;
int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1;
+ int nTotalCla = 0;
// start the bitmap to mark objects that cannot be abstracted because of refinement
// currently, this bitmap is empty because abstraction begins without refinement
Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
@@ -1059,7 +1077,7 @@ 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)
- if ( pPars->fProofRefine )
+ if ( pPars->fAbs2 || pPars->fProofRefine )
{
if ( vBlacks == NULL )
vBlacks = Wlc_NtkGetBlacks( p, pPars );
@@ -1247,6 +1265,13 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
// spurious CEX, continue solving
vClauses = IPdr_ManSaveClauses( pPdr, 0 );
+ if ( vClauses && pPars->fVerbose )
+ {
+ int i;
+ Vec_Ptr_t * vVec;
+ Vec_VecForEachLevel( vClauses, vVec, i )
+ nTotalCla += Vec_PtrSize( vVec );
+ }
Pdr_ManStop( pPdr );
@@ -1291,6 +1316,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Abc_PrintTime( 1, "Time", tTotal );
if ( pPars->fVerbose )
+ Abc_Print( 1, "PDRA reused %d clauses.\n", nTotalCla );
+ if ( pPars->fVerbose )
{
ABC_PRTP( "PDR ", tPdr, tTotal );
ABC_PRTP( "CEX Refine ", tCbr, tTotal );
@@ -1321,6 +1348,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
abctime clk = Abc_Clock();
+ Vec_Int_t * vBlacks = NULL;
int nIters, nNodes, nDcFlops, RetValue = -1;
// start the bitmap to mark objects that cannot be abstracted because of refinement
// currently, this bitmap is empty because abstraction begins without refinement
@@ -1347,9 +1375,22 @@ 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 );
+ if ( pPars->fAbs2 )
+ {
+ if ( vBlacks == NULL )
+ vBlacks = Wlc_NtkGetBlacks( p, pPars );
+ else
+ Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
+ pAbs = Wlc_NtkAbs2( p, vBlacks, NULL );
+ vPisNew = Vec_IntDup( vBlacks );
+ }
+ else
+ {
+ 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 );
// if the abstraction has flops with DC-init state,
@@ -1407,6 +1448,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Vec_IntFree( vRefine );
Abc_CexFree( pCex );
}
+ Vec_IntFree( vBlacks );
Vec_BitFree( vUnmark );
// report the result
if ( pPars->fVerbose )
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index a10310d4..8f474f45 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, "AMXFILabrcpmuxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdipmuxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -547,6 +547,12 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
pPars->fCheckClauses ^= 1;
break;
+ case 'd':
+ pPars->fAbs2 ^= 1;
+ break;
+ case 'i':
+ pPars->fProofUsePPI ^= 1;
+ break;
case 'p':
pPars->fPushClauses ^= 1;
break;
@@ -576,7 +582,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
- Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxuvwh]\n" );
+ Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdipmxuvwh]\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 );
@@ -589,6 +595,8 @@ usage:
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-d : toggle using another way of creating abstractions [default = %s]\n", pPars->fAbs2? "yes": "no" );
+ Abc_Print( -2, "\t-i : toggle using PPI values in proof-based refinement [default = %s]\n", pPars->fProofUsePPI? "yes": "no" );
Abc_Print( -2, "\t-u : toggle checking combinationally unsat [default = %s]\n", pPars->fCheckCombUnsat? "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" );
@@ -617,7 +625,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, "AMXFILxvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILdxvwh" ) ) != EOF )
{
switch ( c )
{
@@ -687,6 +695,9 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nLimit < 0 )
goto usage;
break;
+ case 'd':
+ pPars->fAbs2 ^= 1;
+ break;
case 'x':
pPars->fXorOutput ^= 1;
break;
@@ -710,7 +721,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Wlc_NtkAbsCore( pNtk, pPars );
return 0;
usage:
- Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-xvwh]\n" );
+ Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-dxvwh]\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 );
@@ -718,6 +729,7 @@ 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-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-d : toggle using another way of creating abstractions [default = %s]\n", pPars->fAbs2? "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-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 e6f25f1e..8c6f8fbe 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -122,6 +122,8 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fProofRefine = 0; // Use proof-based refinement
pPars->fHybrid = 1; // Use a hybrid of CBR and PBR
pPars->fCheckCombUnsat = 0; // Check if ABS becomes comb. unsat
+ pPars->fAbs2 = 0; // Use UFAR style createAbs
+ pPars->fProofUsePPI = 0; // Use PPI values in PBR
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 04:17:10 +0000