Skip to content

A
abc
Commit cd2bd708 by Alan Mishchenko
Options

Added switch 'dch -r' to skip choices with structural support redundancy.

parent c1f4545e
Showing with 70 additions and 10 deletions
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;
......
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
......
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
......
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",
......
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,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment