diff options
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 76 |
1 files changed, 63 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 151d05c9..8322f27c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7293,15 +7293,17 @@ usage: ***********************************************************************/ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int fVerbose ); + extern Gia_Man_t * Gia_ManFindExact( word * pTruth, int nVars, int nFunc, int nMaxDepth, int * pArrivalTimes, int nBTLimit, int nStartGates, int fVerbose ); - int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0; + int c, nMaxDepth = -1, fMakeAIG = 0, fTest = 0, fVerbose = 0, nVars = 0, nVarsTmp, nFunc = 0, nStartGates = 1, nBTLimit = 100; + char * p1, * p2; word pTruth[64]; + int pArrTimeProfile[8], fHasArrTimeProfile = 0; Abc_Ntk_t * pNtkRes; Gia_Man_t * pGiaRes; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Datvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "DASCatvh" ) ) != EOF ) { switch ( c ) { @@ -7316,6 +7318,51 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nMaxDepth < 0 ) goto usage; break; + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + fHasArrTimeProfile = 1; + p1 = p2 = argv[globalUtilOptind++]; + while ( true ) { + if ( *p2 == ',' ) + { + *p2 = '\0'; + pArrTimeProfile[nVars++] = atoi( p1 ); + *p2++ = ','; + p1 = p2; + } + else if ( *p2 == '\0' ) + { + pArrTimeProfile[nVars++] = atoi( p1 ); + break; + } + else + ++p2; + } + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + nStartGates = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nStartGates < 1 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; case 'a': fMakeAIG ^= 1; break; @@ -7372,7 +7419,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fMakeAIG ) { - pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose ); + pGiaRes = Gia_ManFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, nStartGates - 1, fVerbose ); if ( pGiaRes ) Abc_FrameUpdateGia( pAbc, pGiaRes ); else @@ -7380,7 +7427,7 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, NULL, fVerbose ); + pNtkRes = Abc_NtkFindExact( pTruth, nVars, nFunc, nMaxDepth, fHasArrTimeProfile ? pArrTimeProfile : NULL, nBTLimit, nStartGates - 1, fVerbose ); if ( pNtkRes ) { Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -7392,16 +7439,19 @@ int Abc_CommandExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: exact [-D <num>] [-atvh] <truth1> <truth2> ...\n" ); + Abc_Print( -2, "usage: exact [-DSC <num>] [-A <list>] [-atvh] <truth1> <truth2> ...\n" ); Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" ); - Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" ); - Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); - Abc_Print( -2, "\t-t : run test suite\n" ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); - Abc_Print( -2, "\t-h : print the command usage\n" ); + Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" ); + Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" ); + Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %s]\n", nStartGates ); + Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts [default = %d]\n", nBTLimit ); + Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" ); + Abc_Print( -2, "\t-t : run test suite\n" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" ); + Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t\n" ); - Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" ); - Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" ); + Abc_Print( -2, "\t This command was contributed by Mathias Soeken from EPFL in July 2016.\n" ); + Abc_Print( -2, "\t The author can be contacted as mathias.soeken at epfl.ch\n" ); return 1; } |