Skip to content

A
abc
Commit 9195192f by Yen-Sheng Ho
Options

%pdra -L: now applies to all types

parent bb3eacf4
Showing with 105 additions and 33 deletions
src/base/wlc/wlc.h
...@@ -169,7 +169,7 @@ struct Wlc_Par_t_ ...@@ -169,7 +169,7 @@ struct Wlc_Par_t_
int nBitsMux; // MUX bit-width int nBitsMux; // MUX bit-width
int nBitsFlop; // flop bit-width int nBitsFlop; // flop bit-width
int nIterMax; // the max number of iterations int nIterMax; // the max number of iterations
int nMuxLimit; // the max number of muxes int nLimit; // the max number of signals
int fXorOutput; // XOR outputs of word-level miter int fXorOutput; // XOR outputs of word-level miter
int fCheckClauses; // Check clauses in the reloaded trace int fCheckClauses; // Check clauses in the reloaded trace
int fPushClauses; // Push clauses in the reloaded trace int fPushClauses; // Push clauses in the reloaded trace
......
src/base/wlc/wlcAbs.c
...@@ -465,21 +465,45 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p ...@@ -465,21 +465,45 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p
return 0; return 0;
} }
static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{ {
Vec_Bit_t * vMuxMark = NULL; Vec_Bit_t * vMarks = NULL;
Vec_Ptr_t * vAdds = Vec_PtrAlloc( 1000 );
Vec_Ptr_t * vMuxes = 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; Wlc_Obj_t * pObj; int i;
Int_Pair_t * pPair; Int_Pair_t * pPair;
if ( pPars->nMuxLimit == ABC_INFINITY ) if ( pPars->nLimit == ABC_INFINITY )
return NULL; return NULL;
vMuxMark = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); vMarks = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
Wlc_NtkForEachObj( p, pObj, i ) Wlc_NtkForEachObj( p, pObj, i )
{ {
if ( pObj->Type == WLC_OBJ_MUX ) { 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 ) if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
{ {
pPair = ABC_ALLOC( Int_Pair_t, 1 ); pPair = ABC_ALLOC( Int_Pair_t, 1 );
...@@ -488,60 +512,103 @@ static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -488,60 +512,103 @@ static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
Vec_PtrPush( vMuxes, pPair ); 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( vMuxes, (int (*)(void))IntPairPtrCompare ) ;
Vec_PtrSort( vFlops, (int (*)(void))IntPairPtrCompare ) ;
Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i )
{ {
if ( i >= pPars->nMuxLimit ) if ( i >= pPars->nLimit ) break;
break; Vec_BitWriteEntry( vMarks, pPair->first, 1 );
Vec_BitWriteEntry( vMuxMark, pPair->first, 1 );
} }
if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th ADD has width = %d\n", i, pPair->second );
if ( i && pPars->fVerbose ) Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i )
Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second ); {
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 ) Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i )
ABC_FREE( pPair ); {
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( vMuxes );
Vec_PtrFree( vFlops );
return vMuxMark; return vMarks;
} }
static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark ) static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{ {
Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ; Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ;
Wlc_Obj_t * pObj; int i, Count[4] = {0}; Wlc_Obj_t * pObj; int i, Count[4] = {0};
Vec_Bit_t * vMuxMark = NULL; Vec_Bit_t * vMarks = NULL;
vMuxMark = Wlc_NtkMarkMuxes( p, pPars ) ; vMarks = Wlc_NtkMarkLimit( p, pPars ) ;
Wlc_NtkForEachObj( p, pObj, i ) 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 ( 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 ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++; {
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; 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 ( 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 ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++; {
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; continue;
} }
if ( pObj->Type == WLC_OBJ_MUX ) if ( pObj->Type == WLC_OBJ_MUX )
{ {
if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux ) if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
{ {
if ( vMuxMark == NULL ) if ( vMarks == NULL )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
else if ( Vec_BitEntry( vMuxMark, i ) ) else if ( Vec_BitEntry( vMarks, i ) )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++; Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
} }
continue; continue;
...@@ -549,12 +616,17 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t ...@@ -549,12 +616,17 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t
if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) ) if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
{ {
if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop ) if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++; {
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; continue;
} }
} }
if ( vMuxMark ) if ( vMarks )
Vec_BitFree( vMuxMark ); Vec_BitFree( vMarks );
if ( pPars->fVerbose ) 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.\n", Count[0], Count[1], Count[2], Count[3] );
return vBlacks; return vBlacks;
...@@ -939,7 +1011,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) ...@@ -939,7 +1011,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
if ( pPars->fProofRefine ) if ( pPars->fProofRefine )
{ {
if ( vBlacks == NULL ) if ( vBlacks == NULL )
vBlacks = Wlc_NtkGetBlacks( p, pPars, vUnmark ); vBlacks = Wlc_NtkGetBlacks( p, pPars );
else else
Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark ); Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew ); pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew );
......
src/base/wlc/wlcCom.c
...@@ -527,9 +527,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -527,9 +527,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
pPars->nMuxLimit = atoi(argv[globalUtilOptind]); pPars->nLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( pPars->nMuxLimit < 0 ) if ( pPars->nLimit < 0 )
goto usage; goto usage;
break; break;
case 'a': case 'a':
...@@ -577,7 +577,7 @@ usage: ...@@ -577,7 +577,7 @@ usage:
Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); 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-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-L num : maximum number of muxes [default = %d]\n", pPars->nMuxLimit ); 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-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-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" );
......
src/base/wlc/wlcNtk.c
...@@ -113,7 +113,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars ) ...@@ -113,7 +113,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
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->nMuxLimit = ABC_INFINITY; // the max number of muxes pPars->nLimit = ABC_INFINITY; // the max number of signals
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
......
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