fold: Option (-s) to make sequential cleanup optional

(cherry picked from commit 1bd088d027)
This commit is contained in:
Jannis Harder 2023-06-07 13:58:51 +02:00 committed by Martin Povišer
parent b23f998b81
commit 6d52a1e449
5 changed files with 16 additions and 9 deletions

View File

@ -114,7 +114,7 @@ extern Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * v
extern int Saig_ManDetectConstrTest( Aig_Man_t * p );
extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigConstr2.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
// -- jlong -- begin
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );

View File

@ -939,7 +939,7 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nCo
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
@ -1000,7 +1000,8 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
// perform cleanup
Aig_ManCleanup( pAigNew );
Aig_ManSeqCleanup( pAigNew );
if ( fSeqCleanup )
Aig_ManSeqCleanup( pAigNew );
return pAigNew;
}

View File

@ -29681,14 +29681,16 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int fCompl;
int fVerbose;
int fSeqCleanup;
int c;
extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup );
pNtk = Abc_FrameReadNtk(pAbc);
// set defaults
fCompl = 0;
fVerbose = 0;
fSeqCleanup = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cvsh" ) ) != EOF )
{
switch ( c )
{
@ -29698,6 +29700,9 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
case 's':
fSeqCleanup ^= 1;
break;
case 'h':
goto usage;
default:
@ -29727,7 +29732,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Abc_NtkIsComb(pNtk) )
Abc_Print( 0, "The network is combinational.\n" );
// modify the current network
pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose );
pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose, fSeqCleanup );
if ( pNtkRes == NULL )
{
Abc_Print( 1,"Transformation has failed.\n" );
@ -29742,6 +29747,7 @@ usage:
Abc_Print( -2, "\t (constraints fail when any of them becomes 1 in any timeframe)\n" );
Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-s : toggle performing sequential cleanup [default = %s]\n", fSeqCleanup? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

View File

@ -4682,7 +4682,7 @@ Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nPr
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
@ -4690,7 +4690,7 @@ Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose, fSeqCleanup );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pMan->pName);

View File

@ -1024,7 +1024,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
pAig = Gia_ManToAigSimple( pAbs );
Gia_ManStop( pAbs );
pAig->nConstrs = 1;
pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 );
pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0, 1 );
Aig_ManStop( pTempAig );
pAbs = Gia_ManFromAigSimple( pAig );
Aig_ManStop( pAig );