From 288d64d033516f992b7c07620e43ee6fbbf9e26a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 16 Sep 2014 14:59:28 -0700 Subject: New choice computation. --- src/aig/gia/giaScript.c | 126 ++++++++++++++++++++++++++++++++++++++++++++++-- src/base/abci/abc.c | 75 ++++++++++++++++++++++++---- src/map/if/ifTune.c | 18 +++---- 3 files changed, 197 insertions(+), 22 deletions(-) diff --git a/src/aig/gia/giaScript.c b/src/aig/gia/giaScript.c index cf58f794..475dfea7 100644 --- a/src/aig/gia/giaScript.c +++ b/src/aig/gia/giaScript.c @@ -18,9 +18,11 @@ ***********************************************************************/ -#include "gia.h" +#include "giaAig.h" #include "base/main/main.h" #include "base/cmd/cmd.h" +#include "proof/dch/dch.h" +#include "opt/dau/dau.h" ABC_NAMESPACE_IMPL_START @@ -344,6 +346,35 @@ void Gia_ManPerformFlow( int fIsMapped, int nAnds, int nLevels, int nLutSize, in } +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager.] + + Description [This duplicator works for AIGs with choices.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Gia_ManOrderPios( Aig_Man_t * p, Gia_Man_t * pOrder ) +{ + Vec_Ptr_t * vPios; + Gia_Obj_t * pObj; + int i; + assert( Aig_ManCiNum(p) == Gia_ManCiNum(pOrder) ); + assert( Aig_ManCoNum(p) == Gia_ManCoNum(pOrder) ); + vPios = Vec_PtrAlloc( Aig_ManCiNum(p) + Aig_ManCoNum(p) ); + Gia_ManForEachObj( pOrder, pObj, i ) + { + if ( Gia_ObjIsCi(pObj) ) + Vec_PtrPush( vPios, Aig_ManCi(p, Gia_ObjCioId(pObj)) ); + else if ( Gia_ObjIsCo(pObj) ) + Vec_PtrPush( vPios, Aig_ManCo(p, Gia_ObjCioId(pObj)) ); + } + return vPios; +} + /**Function************************************************************* Synopsis [] @@ -355,9 +386,98 @@ void Gia_ManPerformFlow( int fIsMapped, int nAnds, int nLevels, int nLutSize, in SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, int fVerbose ) +Gia_Man_t * Gia_ManAigSynch2Choices( Gia_Man_t * pGia1, Gia_Man_t * pGia2, Gia_Man_t * pGia3, Dch_Pars_t * pPars ) +{ + Aig_Man_t * pMan, * pTemp; + Gia_Man_t * pGia, * pMiter; + // derive miter + Vec_Ptr_t * vPios, * vGias = Vec_PtrAlloc( 3 ); + if ( pGia3 ) Vec_PtrPush( vGias, pGia3 ); + if ( pGia2 ) Vec_PtrPush( vGias, pGia2 ); + if ( pGia1 ) Vec_PtrPush( vGias, pGia1 ); + pMiter = Gia_ManChoiceMiter( vGias ); + Vec_PtrFree( vGias ); + // transform into an AIG + pMan = Gia_ManToAigSkip( pMiter, 3 ); + Gia_ManStop( pMiter ); + // compute choices + pMan = Dch_ComputeChoices( pTemp = pMan, pPars ); + Aig_ManStop( pTemp ); + // reconstruct the network + vPios = Gia_ManOrderPios( pMan, pGia1 ); + pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vPios ); + // convert to GIA + pGia = Gia_ManFromAigChoices( pMan ); + Aig_ManStop( pMan ); + return pGia; +} +Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * pInit, void * pPars0, int nLutSize ) { - return NULL; + extern Gia_Man_t * Gia_ManLutBalance( Gia_Man_t * p, int nLutSize, int fUseMuxes, int fRecursive, int fOptArea, int fVerbose ); + Dch_Pars_t * pParsDch = (Dch_Pars_t *)pPars0; + Gia_Man_t * pGia1, * pGia2, * pGia3, * pNew, * pTemp; + int fVerbose = pParsDch->fVerbose; + Jf_Par_t Pars, * pPars = &Pars; + Lf_ManSetDefaultPars( pPars ); + pPars->fCutMin = 1; + pPars->fCoarsen = 1; + pPars->nRelaxRatio = 20; + pPars->nAreaTuner = 1; + pPars->nCutNum = 4; + pPars->fVerbose = fVerbose; + if ( fVerbose ) Gia_ManPrintStats( pInit, NULL ); + pGia1 = Gia_ManDup( pInit ); + if ( Gia_ManAndNum(pGia1) == 0 ) + { + Gia_ManTransferTiming( pGia1, pInit ); + return pGia1; + } + if ( pGia1->pManTime && pGia1->vLevels == NULL ) + Gia_ManLevelWithBoxes( pGia1 ); + // unmap if mapped + if ( Gia_ManHasMapping(pInit) ) + { + Gia_ManTransferMapping( pGia1, pInit ); + pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( pTemp = pGia1, 0 ); + Gia_ManStop( pTemp ); + } + // perform LUT balancing + pGia2 = Gia_ManLutBalance( pGia1, nLutSize, 1, 1, 1, 0 ); + // perform balancing + pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 ); + if ( fVerbose ) Gia_ManPrintStats( pGia2, NULL ); + Gia_ManStop( pTemp ); + // perform mapping + pGia2 = Lf_ManPerformMapping( pTemp = pGia2, pPars ); + if ( fVerbose ) Gia_ManPrintStats( pGia2, NULL ); + if ( pTemp != pGia2 ) + Gia_ManStop( pTemp ); + // perform balancing + if ( pParsDch->fLightSynth ) + pGia3 = Gia_ManAreaBalance( pGia2, 0, ABC_INFINITY, 0, 0 ); + else + { + pGia2 = Gia_ManAreaBalance( pTemp = pGia2, 0, ABC_INFINITY, 0, 0 ); + if ( fVerbose ) Gia_ManPrintStats( pGia2, NULL ); + Gia_ManStop( pTemp ); + // perform DSD balancing + pGia3 = Gia_ManPerformDsdBalance( pGia2, 6, 8, 0, 0 ); + } + if ( fVerbose ) Gia_ManPrintStats( pGia3, NULL ); + // perform choice computation + pNew = Gia_ManAigSynch2Choices( pGia1, pGia2, pGia3, pParsDch ); + Gia_ManStop( pGia1 ); + Gia_ManStop( pGia2 ); + Gia_ManStop( pGia3 ); + // copy names + ABC_FREE( pNew->pName ); + ABC_FREE( pNew->pSpec ); + pNew->pName = Abc_UtilStrsav(pInit->pName); + pNew->pSpec = Abc_UtilStrsav(pInit->pSpec); + Gia_ManTransferTiming( pNew, pInit ); + return pNew; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ca7be1d9..dad29ae5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28453,16 +28453,66 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, int fVerbose ); + extern Gia_Man_t * Gia_ManAigSynch2( Gia_Man_t * p, void * pPars, int nLutSize ); Gia_Man_t * pTemp; - int c, fVerbose = 0; + Dch_Pars_t Pars, * pPars = &Pars; + int c, nLutSize = 6; + // set defaults + Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSKfvh" ) ) != EOF ) { switch ( c ) { + case 'W': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nWords = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nWords < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nSatVarMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nSatVarMax < 0 ) + goto usage; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by a char string.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'f': + pPars->fLightSynth ^= 1; + break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -28472,18 +28522,23 @@ int Abc_CommandAbc9Synch2( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9Synch2(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9Dch(): There is no AIG.\n" ); return 1; } - pTemp = Gia_ManAigSynch2( pAbc->pGia, fVerbose ); + pTemp = Gia_ManAigSynch2( pAbc->pGia, pPars, nLutSize ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &synch2 [-vh]\n" ); - Abc_Print( -2, "\t performs synthesis and computes structural choices\n" ); - Abc_Print( -2, "\t-v : toggles printing additional information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "usage: &synch2 [-WCSK num] [-fvh]\n" ); + Abc_Print( -2, "\t computes structural choices using a new approach\n" ); + Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax ); + Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index d21ebad0..400520e6 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -394,14 +394,14 @@ void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual ) { word Cond[4], Equa[4], Temp[4]; word s_TtElems[8][4] = { - ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA), - ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC), - ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0), - ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00), - ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000), - ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000), - ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF), - ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) + { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA) }, + { ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC) }, + { ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0) }, + { ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00) }, + { ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000) }, + { ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000) }, + { ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF) }, + { ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) } }; int i, nWords = Abc_TtWordNum(2*nVars); assert( nVars > 0 && nVars <= 4 ); @@ -528,7 +528,7 @@ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat ) int nSatVars = sat_solver_nvars(pSat); for ( i = 0; i < p->nObjs-1; i++ ) p->Nodes[i].Var = nSatVars++; - p->Nodes[p->nObjs-1].Var = -ABC_INFINITY; + p->Nodes[p->nObjs-1].Var = 0xFFFF; sat_solver_setnvars( pSat, nSatVars ); // verify variable values for ( i = 0; i < p->nVars; i++ ) -- cgit v1.2.3