summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2021-07-31 15:34:46 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2021-07-31 15:34:46 -0700
commit692dd763190d2e2682c0eeabdcd81f16aaaabe94 (patch)
treea62ab7910e947f5967b90b527fdbaaf4785ee607
parentd925e4802cdbd89b1c7cee4fa1041b08cf0d32f7 (diff)
downloadabc-692dd763190d2e2682c0eeabdcd81f16aaaabe94.tar.gz
abc-692dd763190d2e2682c0eeabdcd81f16aaaabe94.tar.bz2
abc-692dd763190d2e2682c0eeabdcd81f16aaaabe94.zip
Upgrading choice computation.
-rw-r--r--src/base/abci/abc.c16
-rw-r--r--src/base/abci/abcDar.c36
-rw-r--r--src/opt/dar/darScript.c4
-rw-r--r--src/proof/cec/cecChoice.c6
-rw-r--r--src/proof/cec/cecSatG2.c3
5 files changed, 38 insertions, 27 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 83c98e10..06a7c877 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -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 );
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ae2d9835..95c9200d 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -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;
-clk = Abc_Clock();
- if ( pPars->fSynthesis )
- pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
- else
+ if ( pPars->fUseNew )
+ pMan = Dar_ManChoiceNew( pMan, pPars );
+ else
{
- pGia = Gia_ManFromAig( pMan );
- Aig_ManStop( pMan );
- }
+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 );
+ }
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 );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index 684e85e6..d95c23d7 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -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
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 780a1196..db0059fd 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -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 );
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 19349986..ae90e7fc 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -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 );
}