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 | |
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')
-rw-r--r-- | src/base/abci/abc.c | 24 | ||||
-rw-r--r-- | src/base/abci/abcExact.c | 30 | ||||
-rw-r--r-- | src/base/abci/abcIf.c | 18 |
3 files changed, 64 insertions, 8 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" ); diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index 1bb7973a..04d2ebee 100644 --- a/src/base/abci/abcExact.c +++ b/src/base/abci/abcExact.c @@ -1003,6 +1003,36 @@ void Abc_ExactTest( int fVerbose ) } +/**Function************************************************************* + + Synopsis [APIs for integraging with the mapper.] + +***********************************************************************/ +// may need to have a static pointer to the SAT-based synthesis engine and/or loaded library +// this procedure should return 1, if the engine/library are available, and 0 otherwise +int Abc_ExactIsRunning() +{ + return 0; +} +// this procedure returns the number of inputs of the library +// for example, somebody may try to map into 10-cuts while the library only contains 8-functions +int Abc_ExactInputNum() +{ + return 0; +} +// this procedure takes input arrival times (pArrTimeProfile) and +// return the output smallest possible output arrival time +int Abc_ExactDelayCost( int nVars, word * pTruth, int * pArrTimeProfile ) +{ + return 0; +} +// this procedure returns a new node whose output in terms of the given fanins whose output +// has the smallest possible arrival time (in agreement with the above Abc_ExactDelayCost) +Abc_Obj_t * Abc_ExactBuildNode( word * pTruth, int nVars, int * pArrTimeProfile, Abc_Obj_t ** pFanins ) +{ + return NULL; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index c45eaec5..85164d04 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -116,7 +116,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ) pPars->pTimesReq = Abc_NtkGetCoRequiredFloats(pNtk); // update timing info to reflect logic level - if ( (pPars->fDelayOpt || pPars->fDsdBalance || pPars->fUserRecLib) && pNtk->pManTime ) + if ( (pPars->fDelayOpt || pPars->fDsdBalance || pPars->fUserRecLib || pPars->fUserSesLib) && pNtk->pManTime ) { int c; if ( pNtk->AndGateDelay == 0.0 ) @@ -318,7 +318,7 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ) // create the new network if ( pIfMan->pPars->fUseBdds || pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); - else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->nGateSize > 0 ) + else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->fUserSesLib || pIfMan->pPars->nGateSize > 0 ) pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); else pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG ); @@ -445,12 +445,20 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t return pNodeNew; assert( pIfObj->Type == IF_AND ); // get the parameters of the best cut + pCutBest = If_ObjCutBest( pIfObj ); + if ( pIfMan->pPars->fUserSesLib ) + { + // create the subgraph composed of Abc_Obj_t nodes based on the given cut + Abc_Obj_t * pFanins[IF_MAX_FUNC_LUTSIZE]; + If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i ) + pFanins[i] = Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf, vCover); + return Abc_ExactBuildNode( If_CutTruthW(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), If_CutArrTimeProfile(pIfMan, pCutBest), pFanins ); + } // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); - pCutBest = If_ObjCutBest( pIfObj ); -// printf( "%d 0x%02X %d\n", pCutBest->nLeaves, 0xff & *If_CutTruth(pCutBest), pIfMan->pPars->pFuncCost(pCutBest) ); // if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays ) - if ( !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->fUseTtPerm && !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->nGateSize ) + if ( !pIfMan->pPars->fDelayOpt && !pIfMan->pPars->fDelayOptLut && !pIfMan->pPars->fDsdBalance && !pIfMan->pPars->fUseTtPerm && + !pIfMan->pPars->pLutStruct && !pIfMan->pPars->fUserRecLib && !pIfMan->pPars->fUserSesLib && !pIfMan->pPars->nGateSize ) If_CutRotatePins( pIfMan, pCutBest ); if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { |