diff options
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fa2aa375..9167c54c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19927,6 +19927,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Does not work for combinational networks.\n" ); return 0; } + if ( Abc_NtkConstrNum(pNtk) > 0 ) + { + Abc_Print( -1, "Constraints have to be folded (use \"fold\").\n" ); + return 0; + } pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); @@ -24162,10 +24167,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ParFra_t Pars, * pPars = &Pars; int c; int nCofFanLit = 0; - int nNewAlgo = 1; + int fNewAlgo = 1; + int fInitSpecial = 0; Gia_ManFraSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FLiavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FLiasvh" ) ) != EOF ) { switch ( c ) { @@ -24195,7 +24201,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fInit ^= 1; break; case 'a': - nNewAlgo ^= 1; + fNewAlgo ^= 1; + break; + case 's': + fInitSpecial ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -24216,9 +24225,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } - if ( nCofFanLit ) + if ( fInitSpecial ) + pTemp = Gia_ManFramesInitSpecial( pAbc->pGia, pPars->nFrames, pPars->fVerbose ); + else if ( nCofFanLit ) pTemp = Gia_ManUnrollAndCofactor( pAbc->pGia, pPars->nFrames, nCofFanLit, pPars->fVerbose ); - else if ( nNewAlgo ) + else if ( fNewAlgo ) pTemp = Gia_ManFrames2( pAbc->pGia, pPars ); else pTemp = Gia_ManFrames( pAbc->pGia, pPars ); @@ -24226,12 +24237,13 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &frames [-FL <num>] [-aivh]\n" ); + Abc_Print( -2, "usage: &frames [-FL <num>] [-iasvh]\n" ); Abc_Print( -2, "\t unrolls the design for several timeframes\n" ); Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames ); Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit ); Abc_Print( -2, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", nNewAlgo? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; |