luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

added an option -L to %pdra for limiting the number of muxes

This commit is contained in:
Yen-Sheng Ho 2017-02-26 15:39:48 -08:00
parent 27bdffd5a2
commit 86b3cb3da9
4 changed files with 85 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/base/wlc/wlc.h
View File

@ -169,6 +169,7 @@ struct Wlc_Par_t_
int nBitsMux; // MUX bit-width
int nBitsFlop; // flop bit-width
int nIterMax; // the max number of iterations
int nMuxLimit; // the max number of muxes
int fXorOutput; // XOR outputs of word-level miter
int fCheckClauses; // Check clauses in the reloaded trace
int fPushClauses; // Push clauses in the reloaded trace

70
src/base/wlc/wlcAbs.c
View File

@ -34,6 +34,18 @@ 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 ///
////////////////////////////////////////////////////////////////////////
@ -455,10 +467,59 @@ static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** p
return 0;
}
static Vec_Bit_t * Wlc_NtkMarkMuxes( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
Vec_Bit_t * vMuxMark = NULL;
Vec_Ptr_t * vMuxes = Vec_PtrAlloc( 1000 );
Wlc_Obj_t * pObj; int i;
Int_Pair_t * pPair;
if ( pPars->nMuxLimit == ABC_INFINITY )
return NULL;
vMuxMark = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
Wlc_NtkForEachObj( p, pObj, i )
{
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 );
}
}
}
Vec_PtrSort( vMuxes, (int (*)(void))IntPairPtrCompare ) ;
Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i )
{
if ( i >= pPars->nMuxLimit )
break;
Vec_BitWriteEntry( vMuxMark, 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 *, vMuxes, pPair, i )
ABC_FREE( pPair );
Vec_PtrFree( vMuxes );
return vMuxMark;
}
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};
Vec_Bit_t * vMuxMark = NULL;
vMuxMark = Wlc_NtkMarkMuxes( p, pPars ) ;
Wlc_NtkForEachObj( p, pObj, i )
{
if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
@ -479,7 +540,12 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t
if ( pObj->Type == WLC_OBJ_MUX )
{
if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
{
if ( vMuxMark == NULL )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
else if ( Vec_BitEntry( vMuxMark, i ) )
Vec_IntPush( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
}
continue;
}
if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
@ -489,6 +555,8 @@ static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t
continue;
}
}
if ( vMuxMark )
Vec_BitFree( vMuxMark );
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;

16
src/base/wlc/wlcCom.c
View File

@ -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, "AMXFIabcpmxvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabcpmxvwh" ) ) != EOF )
{
switch ( c )
{
@ -521,6 +521,17 @@ 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->nMuxLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMuxLimit < 0 )
goto usage;
break;
case 'a':
pPars->fPdra ^= 1;
break;
@ -559,13 +570,14 @@ 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] [-abcpmxvwh]\n" );
Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abcpmxvwh]\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 muxes [default = %d]\n", pPars->nMuxLimit );
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" );

1
src/base/wlc/wlcNtk.c
View File

@ -113,6 +113,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
pPars->nIterMax = 1000; // the max number of iterations
pPars->nMuxLimit = ABC_INFINITY; // the max number of muxes
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