summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaBalance.c53
-rw-r--r--src/aig/gia/giaIf.c32
-rw-r--r--src/base/abci/abc.c45
-rw-r--r--src/opt/dar/darLib.c2
-rw-r--r--src/sat/bmc/bmcBmcAnd.c4
-rw-r--r--src/sat/bmc/bmcMulti.c2
7 files changed, 119 insertions, 22 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e12b66e2..d509d856 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1021,7 +1021,7 @@ extern void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFile
/*=== giaBalance.c ===========================================================*/
extern Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
extern Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
-extern Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose );
extern Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
extern Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
/*=== giaBidec.c ===========================================================*/
@@ -1186,6 +1186,7 @@ extern void Gia_ManMappingVerify( Gia_Man_t * p );
extern void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p );
extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars, int fNormalized );
extern Gia_Man_t * Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
+extern Gia_Man_t * Gia_ManPerformDsdBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
/*=== giaJf.c ===========================================================*/
extern void Jf_ManSetDefaultPars( Jf_Par_t * pPars );
extern Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index 611bbf87..65c87387 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -1017,7 +1017,7 @@ void Gia_ManAigTransferPiLevels( Gia_Man_t * pNew, Gia_Man_t * p )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
@@ -1029,18 +1029,65 @@ Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutM
else
{
Lf_ManSetDefaultPars( pPars );
- pPars->fCoarsen = fCoarsen;
pPars->fCutMin = fCutMin;
+ pPars->fCoarsen = fCoarsen;
pPars->nRelaxRatio = nRelaxRatio;
pPars->nAreaTuner = 1;
+ pPars->nCutNum = 4;
}
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
+ p = Gia_ManDup( pTemp = p );
+ Gia_ManAigTransferPiLevels( p, pTemp );
if ( Gia_ManAndNum(p) == 0 )
- return Gia_ManDup(p);
+ return p;
+ // delay optimization
+ if ( fDelayMin )
+ {
+ int Area0, Area1, Delay0, Delay1;
+ int fCutMin = pPars->fCutMin;
+ int fCoarsen = pPars->fCoarsen;
+ int nRelaxRatio = pPars->nRelaxRatio;
+ pPars->fCutMin = 0;
+ pPars->fCoarsen = 0;
+ pPars->nRelaxRatio = 0;
+ // perform mapping
+ if ( fOldAlgo )
+ Jf_ManPerformMapping( p, pPars );
+ else
+ Lf_ManPerformMapping( p, pPars );
+ Area0 = (int)pPars->Area;
+ Delay0 = (int)pPars->Delay;
+ // perform balancing
+ pNew = Gia_ManPerformDsdBalance( p, 4, 0, 0 );
+ // perform mapping again
+ if ( fOldAlgo )
+ Jf_ManPerformMapping( pNew, pPars );
+ else
+ Lf_ManPerformMapping( pNew, pPars );
+ Area1 = (int)pPars->Area;
+ Delay1 = (int)pPars->Delay;
+ // choose the best result
+ if ( Delay1 < Delay0 - 1 || (Delay1 == Delay0 + 1 && 100.0 * (Area1 - Area0) / Area1 < 3.0) )
+ {
+ Gia_ManAigTransferPiLevels( pNew, p );
+ Gia_ManStop( p );
+ p = pNew;
+ }
+ else
+ {
+ Gia_ManStop( pNew );
+ Vec_IntFreeP( &p->vMapping );
+ }
+ // reset params
+ pPars->fCutMin = fCutMin;
+ pPars->fCoarsen = fCoarsen;
+ pPars->nRelaxRatio = nRelaxRatio;
+ }
// perform balancing
pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManAigTransferPiLevels( pNew, p );
+ Gia_ManStop( p );
// perform mapping
if ( fOldAlgo )
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index a3ebf305..61b40117 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1758,6 +1758,38 @@ Gia_Man_t * Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRati
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
+Gia_Man_t * Gia_ManPerformDsdBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose )
+{
+ Gia_Man_t * pNew;
+ If_Man_t * pIfMan;
+ If_Par_t Pars, * pPars = &Pars;
+ If_ManSetDefaultPars( pPars );
+ pPars->nCutsMax = nCutNum;
+ pPars->nRelaxRatio = nRelaxRatio;
+ pPars->fVerbose = fVerbose;
+ pPars->nLutSize = 6;
+ pPars->fDsdBalance = 1;
+ pPars->fUseDsd = 1;
+ pPars->fCutMin = 1;
+ pPars->fTruth = 1;
+ pPars->fExpRed = 0;
+ if ( Abc_FrameReadManDsd() == NULL )
+ Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, 0) );
+ // perform mapping
+ pIfMan = Gia_ManToIf( p, pPars );
+ pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
+ if ( pPars->fDsdBalance )
+ If_DsdManAllocIsops( pIfMan->pIfDsdMan, pPars->nLutSize );
+ If_ManPerformMapping( pIfMan );
+ pNew = Gia_ManFromIfAig( pIfMan );
+ If_ManStop( pIfMan );
+ // transfer name
+ assert( pNew->pName == NULL );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+ return pNew;
+}
/**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 32786a94..dff328eb 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10603,16 +10603,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Nf_ManPrepareLibraryTest();
// return 0;
}
-
+/*
if ( pNtk )
{
- extern Abc_Ntk_t * Abc_NtkBarBufsOnOffTest( Abc_Ntk_t * pNtk );
- Abc_Ntk_t * pNtkRes = Abc_NtkBarBufsOnOffTest( pNtk );
-// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fNewAlgo, int fVerbose );
+// extern Abc_Ntk_t * Abc_NtkBarBufsOnOffTest( Abc_Ntk_t * pNtk );
+// Abc_Ntk_t * pNtkRes = Abc_NtkBarBufsOnOffTest( pNtk );
+ extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fNewAlgo, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkPcmTestAig( Abc_Ntk_t * pNtk, int fVerbose );
-// Abc_Ntk_t * pNtkRes;
+ Abc_Ntk_t * pNtkRes;
// if ( Abc_NtkIsLogic(pNtk) )
-// pNtkRes = Abc_NtkPcmTest( pNtk, fNewAlgo, fVerbose );
+ pNtkRes = Abc_NtkPcmTest( pNtk, fNewAlgo, fVerbose );
// else
// pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
if ( pNtkRes == NULL )
@@ -10622,6 +10622,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
+*/
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@@ -27936,9 +27937,10 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCoarsen = 1;
int fCutMin = 0;
int nRelaxRatio = 20;
+ int fDelayMin = 1;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Rakmvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Rakmdvwh" ) ) != EOF )
{
switch ( c )
{
@@ -27962,6 +27964,9 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fCutMin ^= 1;
break;
+ case 'd':
+ fDelayMin ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -27979,19 +27984,29 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Syn2(): There is no AIG.\n" );
return 1;
}
- pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fVerbose, fVeryVerbose );
+ if ( fDelayMin )
+ {
+ If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd();
+ if ( p && If_DsdManVarNum(p) < 6 )
+ {
+ printf( "DSD manager has incompatible number of variables. Delay minimization is not performed.\n" );
+ fDelayMin = 0;
+ }
+ }
+ pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fDelayMin, fVerbose, fVeryVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &syn2 [-R num] [-akmlvh]\n" );
+ Abc_Print( -2, "usage: &syn2 [-R num] [-akmdvh]\n" );
Abc_Print( -2, "\t performs AIG optimization\n" );
- Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
- Abc_Print( -2, "\t-a : toggles using the old algorithm [default = %s]\n", fOldAlgo? "yes": "no" );
- Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", fCoarsen? "yes": "no" );
- Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", fCutMin? "yes": "no" );
- Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
- Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
+ Abc_Print( -2, "\t-a : toggles using the old algorithm [default = %s]\n", fOldAlgo? "yes": "no" );
+ Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", fCoarsen? "yes": "no" );
+ Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", fCutMin? "yes": "no" );
+ Abc_Print( -2, "\t-d : toggles additional delay optimization [default = %s]\n", fDelayMin? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c
index 339cd316..1a41d902 100644
--- a/src/opt/dar/darLib.c
+++ b/src/opt/dar/darLib.c
@@ -593,6 +593,8 @@ Dar_Lib_t * Dar_LibRead()
void Dar_LibStart()
{
// abctime clk = Abc_Clock();
+ if ( s_DarLib != NULL )
+ return;
assert( s_DarLib == NULL );
s_DarLib = Dar_LibRead();
// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index d8b063ce..406aead1 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -786,7 +786,7 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pPars->fUseSynth )
{
Gia_Man_t * pTemp = p->pFrames;
- p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, pPars->fVerbose, 0 );
+ p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, 0, pPars->fVerbose, 0 );
Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
@@ -970,7 +970,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
}
if ( pPars->fUseSynth )
{
- p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
+ p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, 0, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL );
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index 71085d62..2dd03f31 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -140,7 +140,7 @@ Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose
Aig_Man_t * pAig;
Gia_Man_t * pGia, * pTemp;
pGia = Gia_ManFromAig( p );
- pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0 );
+ pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0, 0 );
Gia_ManStop( pTemp );
pAig = Gia_ManToAig( pGia, 0 );
Gia_ManStop( pGia );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 22:01:26 +0000