diff options
| -rw-r--r-- | src/aig/gia/giaQbf.c | 17 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 15 |
2 files changed, 24 insertions, 8 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 247c3dad..f32db0a4 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -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 diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ad7257f0..a5251c7a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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; |