luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Upgrading choice computation.

This commit is contained in:
Alan Mishchenko 2021-07-31 15:34:46 -07:00
parent d925e4802c
commit 692dd76319
5 changed files with 38 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/base/abci/abc.c
View File

@ -15125,7 +15125,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, "WCSsptgcfrvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfrxvh" ) ) != EOF )
{
switch ( c )
{
@ -15183,6 +15183,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
pPars->fSkipRedSupp ^= 1;
break;
case 'x':
pPars->fUseNew ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -15213,7 +15216,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrvh]\n" );
Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrxvh]\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 );
@ -15225,6 +15228,7 @@ usage:
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-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "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;
@ -30654,7 +30658,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
else
{
Abc_Ntk_t * pNtkNoCh;
// Abc_Print( -1, "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pGia) );
Abc_Print( -1, "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pGia) );
// create network without choices
pMan = Gia_ManToAig( pAbc->pGia, 0 );
pNtkNoCh = Abc_NtkFromAigPhase( pMan );
@ -32565,19 +32569,19 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( nVars )
{
Abc_Print( -1, "Cofactoring the last %d inputs.\n", nVars );
Abc_Print( 0, "Cofactoring the last %d inputs.\n", nVars );
pTemp = Gia_ManComputeCofs( pAbc->pGia, nVars );
Abc_FrameUpdateGia( pAbc, pTemp );
}
else if ( nLimFan )
{
Abc_Print( -1, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
Abc_Print( 0, "Cofactoring all variables whose fanout count is higher than %d.\n", nLimFan );
pTemp = Gia_ManDupCofAll( pAbc->pGia, nLimFan, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
}
else if ( iVar )
{
Abc_Print( -1, "Cofactoring one variable with object ID %d.\n", iVar );
Abc_Print( 0, "Cofactoring one variable with object ID %d.\n", iVar );
pTemp = Gia_ManDupCof( pAbc->pGia, iVar );
Abc_FrameUpdateGia( pAbc, pTemp );
}

36
src/base/abci/abcDar.c
View File

@ -1651,6 +1651,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
***********************************************************************/
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
@ -1662,23 +1663,28 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
pMan = Abc_NtkToDar( pNtk, 0, 0 );
if ( pMan == NULL )
return NULL;
if ( pPars->fUseNew )
pMan = Dar_ManChoiceNew( pMan, pPars );
else
{
clk = Abc_Clock();
if ( pPars->fSynthesis )
pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
else
{
pGia = Gia_ManFromAig( pMan );
Aig_ManStop( pMan );
}
if ( pPars->fSynthesis )
pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
else
{
pGia = Gia_ManFromAig( pMan );
Aig_ManStop( pMan );
}
pPars->timeSynth = Abc_Clock() - clk;
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else
{
pMan = Gia_ManToAigSkip( pGia, 3 );
Gia_ManStop( pGia );
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else
{
pMan = Gia_ManToAigSkip( pGia, 3 );
Gia_ManStop( pGia );
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
}
}
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );

4
src/opt/dar/darScript.c
View File

@ -848,7 +848,7 @@ pPars->timeSynth = Abc_Clock() - clk;
***********************************************************************/
Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
@ -872,7 +872,7 @@ pPars->timeSynth = Abc_Clock() - clk;
// perform choice computation
if ( pPars->fUseNew )
pMan = Cec_ComputeChoicesNew( pGia, pPars->fVerbose );
pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
else if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else

6
src/proof/cec/cecChoice.c
View File

@ -412,11 +412,11 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
SeeAlso []
***********************************************************************/
Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose )
Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose );
extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose );
Aig_Man_t * pAig;
Cec4_ManSimulateTest2( pGia, fVerbose );
Cec4_ManSimulateTest2( pGia, nConfs, fVerbose );
pGia = Gia_ManEquivToChoices( pGia, 3 );
Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
pAig = Gia_ManToAig( pGia, 1 );

3
src/proof/cec/cecSatG2.c
View File

@ -1794,13 +1794,14 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars )
Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
return pNew;
}
void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose )
void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose )
{
abctime clk = Abc_Clock();
Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Cec4_ManSetParams( pPars );
Cec4_ManPerformSweeping( p, pPars, NULL, 0 );
pPars->fVerbose = fVerbose;
pPars->nBTLimit = nConfs;
if ( fVerbose )
Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk );
}