From 6d52a1e44999ac19d53d9a8204cc5276db9cdc81 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 7 Jun 2023 13:58:51 +0200 Subject: [PATCH] fold: Option (-s) to make sequential cleanup optional (cherry picked from commit 1bd088d027262bc66c6ec2f1ca65c338c71dd168) --- src/aig/saig/saig.h | 2 +- src/aig/saig/saigConstr2.c | 5 +++-- src/base/abci/abc.c | 12 +++++++++--- src/base/abci/abcDar.c | 4 ++-- src/base/wlc/wlcMem.c | 2 +- 5 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 16e7fb442..4744b8f86 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -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 ); diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index 6e560b59e..79f557616 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -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; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a78706032..17e5b2905 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -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; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 76c7cf547..a209143f3 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -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); diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c index b2d5c5ee0..1f35f324e 100644 --- a/src/base/wlc/wlcMem.c +++ b/src/base/wlc/wlcMem.c @@ -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 );