diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-29 16:03:42 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-29 16:03:42 -0700 |
commit | fb33d69db8fbdffc00f0125550e67990a8fba4b0 (patch) | |
tree | f9423e8b0bb12844bcc88e46a0275cea80896a11 /src/base/abci/abc.c | |
parent | 02d56ea04cb93c41517b748da858a5ae3ba419c7 (diff) | |
download | abc-fb33d69db8fbdffc00f0125550e67990a8fba4b0.tar.gz abc-fb33d69db8fbdffc00f0125550e67990a8fba4b0.tar.bz2 abc-fb33d69db8fbdffc00f0125550e67990a8fba4b0.zip |
Infrastructure for using the results of exact SAT-based synthesis during mapping.
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 24 |
1 files changed, 21 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 244255da..703fd63d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -16495,7 +16495,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) If_ManSetDefaultPars( pPars ); pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut(); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyojiktncvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYDEWSqaflepmrsdbgxyuojiktncvh" ) ) != EOF ) { switch ( c ) { @@ -16700,6 +16700,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'y': pPars->fUserRecLib ^= 1; break; + case 'u': + pPars->fUserSesLib ^= 1; + break; case 'o': pPars->fUseBuffs ^= 1; break; @@ -16843,7 +16846,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fExpRed = 0; } // modify the subgraph recording - if ( pPars->fUserRecLib ) + if ( pPars->fUserRecLib || pPars->fUserSesLib ) { pPars->fTruth = 1; pPars->fCutMin = 1; @@ -16921,6 +16924,20 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } } + + if ( pPars->fUserSesLib ) + { + if ( !Abc_ExactIsRunning() ) + { + printf( "LMS manager is not running (use \"rec_start3\").\n" ); + return 0; + } + if ( Abc_ExactInputNum() != pPars->nLutSize ) + { + printf( "The number of library inputs (%d) different from the K parameters (%d).\n", Abc_ExactInputNum(), pPars->nLutSize ); + return 0; + } + } // complain if truth tables are requested but the cut size is too large if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE ) @@ -16984,7 +17001,7 @@ usage: sprintf(LutSize, "library" ); else sprintf(LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: if [-KCFAGRNTXY num] [-DEW float] [-S str] [-qarlepmsdbgxyojiktncvh]\n" ); + Abc_Print( -2, "usage: if [-KCFAGRNTXY num] [-DEW float] [-S str] [-qarlepmsdbgxyuojiktncvh]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -17013,6 +17030,7 @@ usage: Abc_Print( -2, "\t-g : toggles delay optimization by SOP balancing [default = %s]\n", pPars->fDelayOpt? "yes": "no" ); Abc_Print( -2, "\t-x : toggles delay optimization by DSD balancing [default = %s]\n", pPars->fDsdBalance? "yes": "no" ); Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" ); + Abc_Print( -2, "\t-u : toggles delay optimization with SAT-based library [default = %s]\n", pPars->fUserSesLib? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" ); Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" ); |