summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h9
-rw-r--r--src/aig/gia/giaBalance.c16
-rw-r--r--src/aig/gia/giaMan.c29
-rw-r--r--src/aig/gia/giaMuxes.c61
-rw-r--r--src/aig/gia/giaResub.c2
-rw-r--r--src/aig/gia/giaSwitch.c1
-rw-r--r--src/aig/gia/giaUtil.c28
-rw-r--r--src/base/abci/abc.c69
-rw-r--r--src/map/if/ifMap.c8
-rw-r--r--src/map/if/ifReduce.c7
-rw-r--r--src/map/mpm/mpmCore.c2
-rw-r--r--src/map/mpm/mpmGates.c2
-rw-r--r--src/proof/cec/cecCec.c11
13 files changed, 141 insertions, 104 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 011f4f91..38f70c9c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -927,10 +927,14 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsMuxId(p, i) ) {} else
#define Gia_ManForEachCi( p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
+#define Gia_ManForEachCiId( p, Id, i ) \
+ for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((Id) = Gia_ObjId(p, Gia_ManCi(p, i))); i++ )
#define Gia_ManForEachCiReverse( p, pObj, i ) \
for ( i = Vec_IntSize(p->vCis) - 1; (i >= 0) && ((pObj) = Gia_ManCi(p, i)); i-- )
#define Gia_ManForEachCo( p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((pObj) = Gia_ManCo(p, i)); i++ )
+#define Gia_ManForEachCoId( p, Id, i ) \
+ for ( i = 0; (i < Vec_IntSize(p->vCos)) && ((Id) = Gia_ObjId(p, Gia_ManCo(p, i))); i++ )
#define Gia_ManForEachCoReverse( p, pObj, i ) \
for ( i = Vec_IntSize(p->vCos) - 1; (i >= 0) && ((pObj) = Gia_ManCo(p, i)); i-- )
#define Gia_ManForEachCoDriver( p, pObj, i ) \
@@ -1172,7 +1176,9 @@ extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName );
extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
/*=== giaMuxes.c ===========================================================*/
-extern Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p );
+extern void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
+extern void Gia_ManPrintMuxStats( Gia_Man_t * p );
+extern Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit );
extern Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p );
/*=== giaPat.c ===========================================================*/
extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
@@ -1282,7 +1288,6 @@ extern Vec_Int_t * Gia_ManRequiredLevel( Gia_Man_t * p );
extern void Gia_ManCreateValueRefs( Gia_Man_t * p );
extern void Gia_ManCreateRefs( Gia_Man_t * p );
extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p );
-extern void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors );
extern int Gia_ManCrossCut( Gia_Man_t * p, int fReverse );
extern int Gia_ManIsNormalized( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index 77b85b48..9760cf39 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -358,7 +358,7 @@ Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose )
{
Gia_Man_t * pNew, * pNew1, * pNew2;
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
- pNew = fSimpleAnd ? Gia_ManDup( p ) : Gia_ManDupMuxes( p );
+ pNew = fSimpleAnd ? Gia_ManDup( p ) : Gia_ManDupMuxes( p, 2 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
pNew1 = Gia_ManBalanceInt( pNew );
if ( fVerbose ) Gia_ManPrintStats( pNew1, NULL );
@@ -958,7 +958,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : p;
if ( fVerbose ) Gia_ManPrintStats( pNew0, NULL );
// derive internal manager
- pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0 );
+ pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0, 2 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
if ( pNew0 != p ) Gia_ManStop( pNew0 );
// perform the operation
@@ -1046,7 +1046,7 @@ Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
- Lf_ManSetDefaultPars( pPars );
+ Jf_ManSetDefaultPars( pPars );
pPars->nRelaxRatio = 40;
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
if ( Gia_ManAndNum(p) == 0 )
@@ -1057,7 +1057,7 @@ Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_ManAigTransferPiLevels( pNew, p );
// perform mapping
pPars->nLutSize = 6;
- pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform balancing
@@ -1067,7 +1067,7 @@ Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_ManStop( pTemp );
// perform mapping
pPars->nLutSize = 4;
- pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform balancing
@@ -1081,7 +1081,7 @@ Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
- Lf_ManSetDefaultPars( pPars );
+ Jf_ManSetDefaultPars( pPars );
pPars->nRelaxRatio = 40;
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
if ( Gia_ManAndNum(p) == 0 )
@@ -1093,7 +1093,7 @@ Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_ManAigTransferPiLevels( pNew, p );
// perform mapping
pPars->nLutSize = 7;
- pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform extraction
@@ -1108,7 +1108,7 @@ Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_ManStop( pTemp );
// perform mapping
pPars->nLutSize = 5;
- pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform extraction
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 3b9e6d3b..f1470287 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -421,32 +421,13 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
Abc_Print( 1, " mem =%5.2f MB", Gia_ManMemory(p)/(1<<20) );
if ( Gia_ManHasDangling(p) )
Abc_Print( 1, " ch =%5d", Gia_ManEquivCountClasses(p) );
- if ( p->pMuxes )
- {
- int nAnds = Gia_ManAndNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p);
- int nXors = Gia_ManXorNum(p);
- int nMuxes = Gia_ManMuxNum(p);
- int nTotal = nAnds + 3*nXors + 3*nMuxes;
- Abc_Print( 1, "\nXOR/MUX stats:" );
- Abc_Print( 1, " xor =%8d (%6.2f %%) ", nXors, 300.0*nXors/nTotal );
- Abc_Print( 1, " mux =%8d (%6.2f %%) ", nMuxes, 300.0*nMuxes/nTotal );
- Abc_Print( 1, " and =%8d (%6.2f %%) ", nAnds, 100.0*nAnds/nTotal );
- }
- else if ( pPars->fMuxXor )
- {
- int nAnds, nMuxes, nXors, nTotal = Gia_ManAndNum(p);
- Gia_ManCountMuxXor( p, &nMuxes, &nXors );
- nAnds = Gia_ManAndNum(p)-3*nMuxes-3*nXors;
- Abc_Print( 1, "\nXOR/MUX stats:" );
- Abc_Print( 1, " xor =%8d (%6.2f %%) ", nXors, 300.0*nXors/nTotal );
- Abc_Print( 1, " mux =%8d (%6.2f %%) ", nMuxes, 300.0*nMuxes/nTotal );
- Abc_Print( 1, " and =%8d (%6.2f %%) ", nAnds, 100.0*nAnds/nTotal );
- }
+ if ( pPars && pPars->fMuxXor )
+ printf( "\nXOR/MUX " ), Gia_ManPrintMuxStats( p );
if ( pPars && pPars->fSwitch )
{
- if ( p->pSwitching )
- Abc_Print( 1, " power =%7.2f", Gia_ManEvaluateSwitching(p) );
- else
+// if ( p->pSwitching )
+// Abc_Print( 1, " power =%7.2f", Gia_ManEvaluateSwitching(p) );
+// else
Abc_Print( 1, " power =%7.2f", Gia_ManComputeSwitching(p, 48, 16, 0) );
}
// Abc_Print( 1, "obj =%5d ", Gia_ManObjNum(p) );
diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c
index b4afe214..db44e219 100644
--- a/src/aig/gia/giaMuxes.c
+++ b/src/aig/gia/giaMuxes.c
@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
- Synopsis [Derives GIA with MUXes.]
+ Synopsis [Counts XORs and MUXes.]
Description []
@@ -42,7 +42,56 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
+void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors )
+{
+ Gia_Obj_t * pObj, * pFan0, * pFan1; int i;
+ *pnMuxes = *pnXors = 0;
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ if ( !Gia_ObjIsMuxType(pObj) )
+ continue;
+ if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+ (*pnXors)++;
+ else
+ (*pnMuxes)++;
+ }
+}
+void Gia_ManPrintMuxStats( Gia_Man_t * p )
+{
+ int nAnds, nMuxes, nXors, nTotal;
+ if ( p->pMuxes )
+ {
+ nAnds = Gia_ManAndNum(p)-Gia_ManXorNum(p)-Gia_ManMuxNum(p);
+ nXors = Gia_ManXorNum(p);
+ nMuxes = Gia_ManMuxNum(p);
+ nTotal = nAnds + 3*nXors + 3*nMuxes;
+ }
+ else
+ {
+ Gia_ManCountMuxXor( p, &nMuxes, &nXors );
+ nAnds = Gia_ManAndNum(p) - 3*nMuxes - 3*nXors;
+ nTotal = Gia_ManAndNum(p);
+ }
+ Abc_Print( 1, "stats: " );
+ Abc_Print( 1, "xor =%8d %6.2f %% ", nXors, 300.0*nXors/nTotal );
+ Abc_Print( 1, "mux =%8d %6.2f %% ", nMuxes, 300.0*nMuxes/nTotal );
+ Abc_Print( 1, "and =%8d %6.2f %% ", nAnds, 100.0*nAnds/nTotal );
+ Abc_Print( 1, "obj =%8d ", Gia_ManAndNum(p) );
+ fflush( stdout );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives GIA with MUXes.]
+
+ Description [Create MUX if the sum of fanin references does not exceed limit.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC;
@@ -51,7 +100,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
ABC_FREE( p->pRefs );
Gia_ManCreateRefs( p );
// start the new manager
- pNew = Gia_ManStart( 5000 );
+ pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
@@ -64,7 +113,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p )
Gia_ManHashStart( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
- if ( !Gia_ObjIsMuxType(pObj) || (Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) > 1 || Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > 1) )
+ if ( !Gia_ObjIsMuxType(pObj) || Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) + Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) > Limit )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
pObj->Value = Gia_ManHashXorReal( pNew, Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan0)), Gia_ObjLitCopy(p, Gia_ObjToLit(p, pFan1)) );
@@ -147,7 +196,7 @@ Gia_Man_t * Gia_ManDupNoMuxes( Gia_Man_t * p )
Gia_Man_t * Gia_ManDupMuxesTest( Gia_Man_t * p )
{
Gia_Man_t * pNew, * pNew2;
- pNew = Gia_ManDupMuxes( p );
+ pNew = Gia_ManDupMuxes( p, 2 );
pNew2 = Gia_ManDupNoMuxes( pNew );
Gia_ManPrintStats( p, NULL );
Gia_ManPrintStats( pNew, NULL );
@@ -277,7 +326,7 @@ void Gia_ManMuxProfiling( Gia_Man_t * p )
Vec_Int_t * vCounts;
int i, nRefs, Size, Count, Total = 0, Roots = 0;
- pNew = Gia_ManDupMuxes( p );
+ pNew = Gia_ManDupMuxes( p, 2 );
Gia_ManCreateRefs( pNew );
Gia_ManForEachCo( pNew, pObj, i )
Gia_ObjRefFanin0Inc( pNew, pObj );
diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
index 4b196fa4..b8c0e294 100644
--- a/src/aig/gia/giaResub.c
+++ b/src/aig/gia/giaResub.c
@@ -261,7 +261,7 @@ void Gia_ManAddDivisors( Gia_Man_t * p, Vec_Wec_t * vMffcs )
void Gia_ManResubTest( Gia_Man_t * p )
{
Vec_Wec_t * vMffcs;
- Gia_Man_t * pNew = Gia_ManDupMuxes( p );
+ Gia_Man_t * pNew = Gia_ManDupMuxes( p, 2 );
abctime clkStart = Abc_Clock();
vMffcs = Gia_ManComputeMffcs( pNew, 4, 100, 8, 100 );
Gia_ManAddDivisors( pNew, vMffcs );
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index 5e97910b..a7b63864 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -758,6 +758,7 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO
// perform the computation of switching activity
vSwitching = Gia_ManComputeSwitchProbs( pDfs, nFrames, nPref, fProbOne );
// transfer the computed result to the original AIG
+ ABC_FREE( p->pSwitching );
p->pSwitching = ABC_CALLOC( unsigned char, Gia_ManObjNum(p) );
pSwitching = (float *)vSwitching->pArray;
Gia_ManForEachObj( p, pObj, i )
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 365a8539..e16ee44f 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -746,34 +746,6 @@ int * Gia_ManCreateMuxRefs( Gia_Man_t * p )
/**Function*************************************************************
- Synopsis [Assigns references.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Gia_ManCountMuxXor( Gia_Man_t * p, int * pnMuxes, int * pnXors )
-{
- Gia_Obj_t * pObj, * pFan0, * pFan1;
- int i;
- *pnMuxes = 0;
- *pnXors = 0;
- Gia_ManForEachAnd( p, pObj, i )
- {
- if ( !Gia_ObjIsMuxType(pObj) )
- continue;
- if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
- (*pnXors)++;
- else
- (*pnMuxes)++;
- }
-}
-
-/**Function*************************************************************
-
Synopsis [Computes the maximum frontier size.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 23873106..ee5a2b93 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -295,8 +295,8 @@ static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFold2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -327,7 +327,7 @@ static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Strash ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Topand ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Add1Hot ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -874,8 +874,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 );
Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 );
- Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong
- Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong
+ Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong
+ Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong
Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 );
Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 );
Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 );
@@ -903,7 +903,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&psig", Abc_CommandAbc9PSig, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&status", Abc_CommandAbc9Status, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&show", Abc_CommandAbc9Show, 0 );
- Cmd_CommandAdd( pAbc, "ABC9", "&st", Abc_CommandAbc9Hash, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&st", Abc_CommandAbc9Strash, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&topand", Abc_CommandAbc9Topand, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&add1hot", Abc_CommandAbc9Add1Hot, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cof", Abc_CommandAbc9Cof, 0 );
@@ -25622,17 +25622,29 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
- int c, fAddStrash = 0;
+ int c, Limit = 2;
+ int fAddStrash = 0;
int fCollapse = 0;
int fAddMuxes = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "acmh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Lacmh" ) ) != EOF )
{
switch ( c )
{
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Limit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Limit < 0 )
+ goto usage;
+ break;
case 'a':
fAddStrash ^= 1;
break;
@@ -25650,11 +25662,18 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
- Abc_Print( -1, "Abc_CommandAbc9Hash(): There is no AIG.\n" );
+ Abc_Print( -1, "Abc_CommandAbc9Strash(): There is no AIG.\n" );
return 1;
}
if ( fAddMuxes )
- pTemp = Gia_ManDupMuxes( pAbc->pGia );
+ {
+ if ( pAbc->pGia->pMuxes )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Strash(): The AIG already has MUXes.\n" );
+ return 1;
+ }
+ pTemp = Gia_ManDupMuxes( pAbc->pGia, Limit );
+ }
else if ( fCollapse && pAbc->pGia->pAigExtra )
{
Gia_Man_t * pNew = Gia_ManDupUnnormalize( pAbc->pGia );
@@ -25663,18 +25682,21 @@ int Abc_CommandAbc9Hash( Abc_Frame_t * pAbc, int argc, char ** argv )
pNew->pManTime = NULL;
Gia_ManStop( pNew );
}
+ else if ( pAbc->pGia->pMuxes )
+ pTemp = Gia_ManDupNoMuxes( pAbc->pGia );
else
pTemp = Gia_ManRehash( pAbc->pGia, fAddStrash );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
- Abc_Print( -2, "usage: &st [-acmh]\n" );
- Abc_Print( -2, "\t performs structural hashing\n" );
- Abc_Print( -2, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
- Abc_Print( -2, "\t-c : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
- Abc_Print( -2, "\t-m : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
- Abc_Print( -2, "\t-h : print the command usage\n");
+ Abc_Print( -2, "usage: &st [-L num] [-acmh]\n" );
+ Abc_Print( -2, "\t performs structural hashing\n" );
+ Abc_Print( -2, "\t-a : toggle additional hashing [default = %s]\n", fAddStrash? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" );
+ Abc_Print( -2, "\t-m : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" );
+ Abc_Print( -2, "\t-L num : create MUX when sum of refs does not exceed this limit [default = %d]\n", Limit );
+ Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -29372,12 +29394,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
nArgcNew = argc - globalUtilOptind;
if ( nArgcNew != 1 )
{
- Abc_Print( -1, "File name is not given on the command line.\n" );
- return 1;
+ if ( pAbc->pGia->pSpec == NULL )
+ {
+ Abc_Print( -1, "File name is not given on the command line.\n" );
+ return 1;
+ }
+ FileName = pAbc->pGia->pSpec;
}
-
- // get the input file name
- FileName = pArgvNew[0];
+ else
+ FileName = pArgvNew[0];
// fix the wrong symbol
for ( pTemp = FileName; *pTemp; pTemp++ )
if ( *pTemp == '>' )
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index c368cbf9..9f709411 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -500,9 +500,11 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
if ( p->pPars->fVerbose )
{
char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
- Abc_Print( 1, "%c: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ",
- Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
-// printf( "Cut0 =%4d. Cut1 =%4d. ", p->nBestCutSmall[0], p->nBestCutSmall[1] );
+ Abc_Print( 1, "%c: Del = %7.2f. Ar = %9.1f. Edge = %8d. ",
+ Symb, p->RequiredGlo, p->AreaGlo, p->nNets );
+ if ( p->dPower )
+ Abc_Print( 1, "Switch = %7.2f. ", p->dPower );
+ Abc_Print( 1, "Cut = %8d. ", p->nCutsMerged );
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
// Abc_Print( 1, "Max number of cuts = %d. Average number of cuts = %5.2f.\n",
// p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
diff --git a/src/map/if/ifReduce.c b/src/map/if/ifReduce.c
index fec999cb..d50bc40c 100644
--- a/src/map/if/ifReduce.c
+++ b/src/map/if/ifReduce.c
@@ -57,8 +57,11 @@ void If_ManImproveMapping( If_Man_t * p )
If_ManComputeRequired( p );
if ( p->pPars->fVerbose )
{
- Abc_Print( 1, "E: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ",
- p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
+ Abc_Print( 1, "E: Del = %7.2f. Ar = %9.1f. Edge = %8d. ",
+ p->RequiredGlo, p->AreaGlo, p->nNets );
+ if ( p->dPower )
+ Abc_Print( 1, "Switch = %7.2f. ", p->dPower );
+ Abc_Print( 1, "Cut = %8d. ", p->nCutsMerged );
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
}
}
diff --git a/src/map/mpm/mpmCore.c b/src/map/mpm/mpmCore.c
index de2d7bc7..1395d1d0 100644
--- a/src/map/mpm/mpmCore.c
+++ b/src/map/mpm/mpmCore.c
@@ -95,7 +95,7 @@ Gia_Man_t * Mpm_ManLutMapping( Gia_Man_t * pGia, Mpm_Par_t * pPars )
assert( pPars->nNumCuts <= MPM_CUT_MAX );
if ( pPars->fUseGates )
{
- pGia = Gia_ManDupMuxes( pGia );
+ pGia = Gia_ManDupMuxes( pGia, 2 );
p = Mig_ManCreate( pGia );
Gia_ManStop( pGia );
}
diff --git a/src/map/mpm/mpmGates.c b/src/map/mpm/mpmGates.c
index aa70e143..d2af268d 100644
--- a/src/map/mpm/mpmGates.c
+++ b/src/map/mpm/mpmGates.c
@@ -287,7 +287,7 @@ Abc_Ntk_t * Mpm_ManCellMapping( Gia_Man_t * pGia, Mpm_Par_t * pPars, void * pMio
assert( pPars->nNumCuts <= MPM_CUT_MAX );
if ( pPars->fUseGates )
{
- pGia = Gia_ManDupMuxes( pGia );
+ pGia = Gia_ManDupMuxes( pGia, 2 );
p = Mig_ManCreate( pGia );
Gia_ManStop( pGia );
}
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index f3b1a3b0..b43700ae 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -66,14 +66,13 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
SeeAlso []
***********************************************************************/
-int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
+int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime clkTotal )
{
// extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
int RetValue, iOut, nOuts;
- abctime clkTotal = Abc_Clock();
if ( piOutFail )
*piOutFail = -1;
Gia_ManStop( pTemp );
@@ -83,12 +82,12 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail )
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
-Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
-Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
if ( pMiterCec->pData == NULL )
Abc_Print( 1, "Counter-example is not available.\n" );
else
@@ -113,7 +112,7 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
else
{
Abc_Print( 1, "Networks are UNDECIDED. " );
-Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );
Aig_ManStop( pMiterCec );
@@ -275,7 +274,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
if ( pPars->fVerbose )
Abc_Print( 1, "Calling the old CEC engine.\n" );
fflush( stdout );
- RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail );
+ RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail, clkTotal );
p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;
if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
Abc_Print( 1, "Counter-example simulation has failed.\n" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-20 20:37:58 +0000