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

Adding new switch to &genqfb to use output as an enable in the miter.

This commit is contained in:
Alan Mishchenko 2019-07-30 17:08:26 +07:00
parent 5776ad07e7
commit 9017fa9169
2 changed files with 24 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/aig/gia/giaQbf.c
View File

@ -132,11 +132,11 @@ Vec_Int_t * Gia_GenCreateMuxes( Gia_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * vFl
}
return vLits;
}
Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSize, char * pStr, int fVerbose )
Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSize, char * pStr, int fUseOut, int fVerbose )
{
Gia_Obj_t * pObj;
Gia_Man_t * pTemp, * pNew;
int i, iMiter, nPars = nLutNum * (1 << nLutSize);
int i, iMiter, iLut0, iLut1, nPars = nLutNum * (1 << nLutSize);
Vec_Int_t * vLits0, * vLits1, * vParLits;
Vec_Int_t * vFlops = Gia_GenCollectFlopIndexes( pStr, nLutNum, nLutSize, Gia_ManRegNum(p) );
// collect parameter literals (data vars)
@ -160,7 +160,18 @@ Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * p, int nFrames, int nLutNum, int nLutSi
vLits0 = Gia_GenCreateMuxes( p, pNew, vFlops, nLutNum, nLutSize, vParLits, 0 );
vLits1 = Gia_GenCreateMuxes( p, pNew, vFlops, nLutNum, nLutSize, vParLits, 1 );
// create miter output
iMiter = Gia_ManHashAnd( pNew, Vec_IntEntry(vLits0, 0), Abc_LitNot(Vec_IntEntry(vLits1, 0)) );
//iMiter = Gia_ManHashAnd( pNew, Vec_IntEntry(vLits0, 0), Abc_LitNot(Vec_IntEntry(vLits1, 0)) );
///////////////////////////////////////////////////////////////////////////
iLut0 = Vec_IntEntry(vLits0, 0);
iLut1 = Vec_IntEntry(vLits1, 0);
if ( fUseOut )
{
Gia_Obj_t * pObjPoLast = Gia_ManPo( p, Gia_ManPoNum(p)-1 );
int iOut = Abc_LitNotCond( Gia_ObjFanin0Copy(pObjPoLast), 0 );
iLut1 = Gia_ManHashAnd( pNew, iLut1, Abc_LitNot(iOut) );
}
iMiter = Gia_ManHashAnd( pNew, iLut0, Abc_LitNot(iLut1) );
///////////////////////////////////////////////////////////////////////////
iMiter = Gia_ManHashAnd( pNew, Abc_LitNot(iMiter), Abc_Var2Lit(1, 0) );
Gia_ManAppendCo( pNew, iMiter );
// cleanup

15
src/base/abci/abc.c
View File

@ -42761,16 +42761,17 @@ usage:
***********************************************************************/
int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * pGia, int nFrames, int nLutNum, int nLutSize, char * pStr, int fVerbose );
extern Gia_Man_t * Gia_GenQbfMiter( Gia_Man_t * pGia, int nFrames, int nLutNum, int nLutSize, char * pStr, int fUseOut, int fVerbose );
int nFrames = 1;
int nLutNum = 1;
int nLutSize = 6;
char * pStr = NULL;
int fUseOut = 0;
int fVerbose = 0;
int c;
Gia_Man_t * pTemp;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FKNSvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FKNSovh" ) ) != EOF )
{
switch ( c )
{
@ -42810,7 +42811,7 @@ int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
Abc_Print( -1, "Command line switch \"-S\" should be followed by a string.\n" );
goto usage;
}
pStr = Abc_UtilStrsav(argv[globalUtilOptind]);
@ -42818,6 +42819,9 @@ int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pStr == NULL )
goto usage;
break;
case 'o':
fUseOut ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -42847,17 +42851,18 @@ int Abc_CommandAbc9GenQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Currently this commands works for one frame and one LUT.\n" );
return 1;
}
pTemp = Gia_GenQbfMiter( pAbc->pGia, nFrames, nLutNum, nLutSize, pStr, fVerbose );
pTemp = Gia_GenQbfMiter( pAbc->pGia, nFrames, nLutNum, nLutSize, pStr, fUseOut, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
ABC_FREE( pStr );
return 0;
usage:
Abc_Print( -2, "usage: &genqbf [-FKN num] [-vh]\n" );
Abc_Print( -2, "usage: &genqbf [-FKN num] [-ovh]\n" );
Abc_Print( -2, "\t generates QBF miter for computing an inductive invariant\n" );
Abc_Print( -2, "\t-F num : the number of time frames for induction [default = %d]\n", nFrames );
Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-N num : the number of LUTs [default = %d]\n", nLutNum );
Abc_Print( -2, "\t-o : toggle using the last output [default = %s]\n", fUseOut? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;