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

Experiment with choice computation.

This commit is contained in:
Alan Mishchenko 2023-02-16 07:14:18 +01:00
parent 38ad178e9e
commit 581c58b9c4
4 changed files with 21 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -42895,7 +42895,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dch_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxyvh" ) ) != EOF )
{
switch ( c )
{
@ -42962,6 +42962,9 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'x':
pPars->fUseNew ^= 1;
break;
case 'y':
pPars->fUseNew2 ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -43001,7 +43004,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxvh]\n" );
Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxyvh]\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 );
@ -43016,6 +43019,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-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" );
Abc_Print( -2, "\t-y : toggle using new choice computation [default = %s]\n", pPars->fUseNew2? "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;

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

@ -849,6 +849,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 nConfs, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoicesNew2( 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 );
@ -873,6 +874,8 @@ pPars->timeSynth = Abc_Clock() - clk;
// perform choice computation
if ( pPars->fUseNew )
pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
else if ( pPars->fUseNew2 )
pMan = Cec_ComputeChoicesNew2( pGia, pPars->nBTLimit, pPars->fVerbose );
else if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else

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

@ -422,6 +422,17 @@ Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose )
Gia_ManStop( pGia );
return pAig;
}
Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose )
{
extern Gia_Man_t * Cec5_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose );
Aig_Man_t * pAig;
Gia_Man_t * pNew = Cec5_ManSimulateTest3( pGia, nConfs, fVerbose );
Gia_ManStop( pNew );
pGia = Gia_ManEquivToChoices( pGia, 3 );
pAig = Gia_ManToAig( pGia, 1 );
Gia_ManStop( pGia );
return pAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

1
src/proof/dch/dch.h
View File

@ -53,6 +53,7 @@ struct Dch_Pars_t_
int fUseGia; // uses GIA package
int fUseCSat; // uses circuit-based solver
int fUseNew; // uses new implementation
int fUseNew2; // uses new implementation
int fLightSynth; // uses lighter version of synthesis
int fSkipRedSupp; // skip choices with redundant support vars
int fVerbose; // verbose stats