summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abc/abcUtil.c22
-rw-r--r--src/base/abci/abc.c7
-rw-r--r--src/base/abci/abcIvy.c28
-rw-r--r--src/base/abci/abcPrint.c3
-rw-r--r--src/base/abci/abcSat.c6
6 files changed, 62 insertions, 5 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index ce1947a9..3d46cdf0 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -814,6 +814,7 @@ extern int Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
extern int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
+extern int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
extern void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
extern int Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index b86dc88f..3070e01a 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -105,7 +105,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
- if ( pNtk->nTravIds == (1<<30)-1 )
+ if ( pNtk->nTravIds >= (1<<30)-1 )
{
pNtk->nTravIds = 0;
Abc_NtkForEachObj( pNtk, pObj, i )
@@ -447,6 +447,26 @@ int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Reads the total number of all fanins.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pNode;
+ int i, nFanins = 0;
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ nFanins += Abc_ObjFaninNum(pNode);
+ return nFanins;
+}
+
+/**Function*************************************************************
+
Synopsis [Cleans the copy field of all objects.]
Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c2a6214d..3a6874ca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2569,6 +2569,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
Res_Par_t Pars, * pPars = &Pars;
int c;
+// printf( "Implementation of this command is not finished.\n" );
+// return 1;
+
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
@@ -2641,8 +2644,8 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" );
- fprintf( pErr, "\t-W <NM> : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
- fprintf( pErr, "\t-S <num> : specifies the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
+ fprintf( pErr, "\t-W <NM> : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
+ fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 243067ce..00f8c183 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -187,18 +187,44 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
{
Abc_Ntk_t * pNtkAig;
Ivy_Man_t * pMan;
+ int clk;
// int i;
-
+/*
+extern int nMoves;
+extern int nMovesS;
+extern int nClauses;
+extern int timeInv;
+
+nMoves = 0;
+nMovesS = 0;
+nClauses = 0;
+timeInv = 0;
+*/
pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
if ( pMan == NULL )
return NULL;
//timeRetime = clock();
+clk = clock();
Ivy_ManHaigStart( pMan, fVerbose );
// Ivy_ManRewriteSeq( pMan, 0, 0 );
// for ( i = 0; i < nIters; i++ )
// Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+
+//printf( "%d ", Ivy_ManNodeNum(pMan) );
Ivy_ManRewriteSeq( pMan, 0, 0 );
+ Ivy_ManRewriteSeq( pMan, 0, 0 );
+ Ivy_ManRewriteSeq( pMan, 1, 0 );
+//printf( "%d ", Ivy_ManNodeNum(pMan) );
+//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
+//PRT( " ", clock() - clk );
+//printf( "\n" );
+/*
+ printf( "Moves = %d. ", nMoves );
+ printf( "MovesS = %d. ", nMovesS );
+ printf( "Clauses = %d. ", nClauses );
+ PRT( "Time", timeInv );
+*/
// Ivy_ManRewriteSeq( pMan, 1, 0 );
//printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
// Ivy_ManHaigPostprocess( pMan, fVerbose );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e66ce018..177c269b 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -77,7 +77,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
// fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
}
else
+ {
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
+ fprintf( pFile, " net = %5d", Abc_NtkGetTotalFanins(pNtk) );
+ }
if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
{
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 96540269..d9cae254 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -65,6 +65,10 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
if ( pSat == NULL )
return 1;
+//printf( "%d \n", pSat->clauses.size );
+//sat_solver_delete( pSat );
+//return 1;
+
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
@@ -619,7 +623,7 @@ void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
nMuxes = 0;
pSat = sat_solver_new();
-sat_solver_store_alloc( pSat );
+//sat_solver_store_alloc( pSat );
RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
sat_solver_store_mark_roots( pSat );
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-14 03:07:04 +0000