From cd2bd70865c6362b8162bef2b3d98125df984b85 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 5 Sep 2012 19:39:25 -0700 Subject: Added switch 'dch -r' to skip choices with structural support redundancy. --- src/base/abci/abc.c | 8 ++++-- src/proof/dch/dch.h | 1 + src/proof/dch/dchChoice.c | 66 ++++++++++++++++++++++++++++++++++++++++++----- src/proof/dch/dchCore.c | 3 ++- src/proof/dch/dchInt.h | 2 +- 5 files changed, 70 insertions(+), 10 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1196cc84..940e2643 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10408,7 +10408,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfrvh" ) ) != EOF ) { switch ( c ) { @@ -10463,6 +10463,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': pPars->fLightSynth ^= 1; break; + case 'r': + pPars->fSkipRedSupp ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -10493,7 +10496,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfvh]\n" ); + Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrvh]\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 ); @@ -10504,6 +10507,7 @@ usage: Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); Abc_Print( -2, "\t-f : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "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/proof/dch/dch.h b/src/proof/dch/dch.h index ff29f0da..e887ba26 100644 --- a/src/proof/dch/dch.h +++ b/src/proof/dch/dch.h @@ -53,6 +53,7 @@ struct Dch_Pars_t_ int fUseGia; // uses GIA package int fUseCSat; // uses circuit-based solver int fLightSynth; // uses lighter version of synthesis + int fSkipRedSupp; // skip choices with redundant support vars int fVerbose; // verbose stats clock_t timeSynth; // synthesis runtime int nNodesAhead; // the lookahead in terms of nodes diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c index 7a763d84..ff8002d9 100644 --- a/src/proof/dch/dchChoice.c +++ b/src/proof/dch/dchChoice.c @@ -185,6 +185,41 @@ static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); } static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); } + + + +/**Function************************************************************* + + Synopsis [Marks the TFI of the node.] + + Description [Returns 1 if there is a CI not marked with previous ID.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) +{ + int RetValue; + if ( pObj == NULL ) + return 0; + if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) + return 0; + if ( Aig_ObjIsCi(pObj) ) + { + RetValue = !Aig_ObjIsTravIdPrevious( p, pObj ); + Aig_ObjSetTravIdCurrent( p, pObj ); + return RetValue; + } + assert( Aig_ObjIsNode(pObj) ); + Aig_ObjSetTravIdCurrent( p, pObj ); + RetValue = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) ); + RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) ); + RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) ); + return (RetValue > 0); +} + /**Function************************************************************* Synopsis [Derives the AIG with choices from representatives.] @@ -196,7 +231,7 @@ static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj SeeAlso [] ***********************************************************************/ -void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj ) +void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps ) { Aig_Obj_t * pRepr, * pObjNew, * pReprNew; // get the new node @@ -227,6 +262,25 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_ // skip choices with combinational loops if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) ) return; + // don't add choice if structural support of pObjNew and pReprNew differ + if ( fSkipRedSupps ) + { + int fSkipChoice = 0; + // mark support of the representative node (pReprNew) + Aig_ManIncrementTravId( pAigNew ); + Dch_ObjMarkTfi_rec( pAigNew, pReprNew ); + // detect if the new node (pObjNew) depends on any additional variables + Aig_ManIncrementTravId( pAigNew ); + if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) ) + fSkipChoice = 1;//, printf( "1" ); + // detect if the representative node (pReprNew) depends on any additional variables + Aig_ManIncrementTravId( pAigNew ); + if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) ) + fSkipChoice = 1;//, printf( "2" ); + // skip the choice if this is what is happening + if ( fSkipChoice ) + return; + } // add choice pAigNew->pEquivs[pObjNew->Id] = pAigNew->pEquivs[pReprNew->Id]; pAigNew->pEquivs[pReprNew->Id] = pObjNew; @@ -260,7 +314,7 @@ Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig ) // construct choices for the internal nodes assert( pAig->pReprs != NULL ); Aig_ManForEachNode( pAig, pObj, i ) - Dch_DeriveChoiceAigNode( pChoices, pAig, pObj ); + Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, 0 ); Aig_ManForEachCo( pAig, pObj, i ) Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); Dch_DeriveChoiceCountEquivs( pChoices ); @@ -442,7 +496,7 @@ void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig ) +Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps ) { Aig_Man_t * pChoices; Aig_Obj_t * pObj; @@ -459,7 +513,7 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig ) // construct choices for the internal nodes assert( pAig->pReprs != NULL ); Aig_ManForEachNode( pAig, pObj, i ) - Dch_DeriveChoiceAigNode( pChoices, pAig, pObj ); + Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps ); Aig_ManForEachCo( pAig, pObj, i ) Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); Dch_DeriveChoiceCountEquivs( pChoices ); @@ -478,12 +532,12 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ) +Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps ) { extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose ); Aig_Man_t * pChoices, * pTemp; int fVerbose = 0; - pChoices = Dch_DeriveChoiceAigInt( pAig ); + pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps ); // pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices ); // Aig_ManStop( pTemp ); // there is no need for cleanup diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index bfef8d8c..0d2e8c0d 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -53,6 +53,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) p->fSimulateTfo = 1; // simulate TFO p->fPower = 0; // power-aware rewriting p->fLightSynth = 0; // uses lighter version of synthesis + p->fSkipRedSupp = 0; // skips choices with redundant structural support p->fVerbose = 0; // verbose stats p->nNodesAhead = 1000; // the lookahead in terms of nodes p->nCallsRecycle = 100; // calls to perform before recycling SAT solver @@ -107,7 +108,7 @@ p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); // create choices ABC_FREE( pAig->pTable ); - pResult = Dch_DeriveChoiceAig( pAig ); + pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp ); // count the number of representatives if ( pPars->fVerbose ) Abc_Print( 1, "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h index 05f4271d..d1dd2c51 100644 --- a/src/proof/dch/dchInt.h +++ b/src/proof/dch/dchInt.h @@ -123,7 +123,7 @@ static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) /*=== dchChoice.c ===================================================*/ extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ); extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ); -extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig ); +extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps ); /*=== dchClass.c =================================================*/ extern Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig ); extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, -- cgit v1.2.3