diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-02-02 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-02-02 08:01:00 -0800 |
commit | 8da52b6f202444711da6b1f1baac92e0a516c8e6 (patch) | |
tree | caa6bf9d35cb8f10785c9e2fc9dd0a179704db33 /src/base/abci | |
parent | 12578e622f62bde4cfc1d3b055aa8747e5c9590b (diff) | |
download | abc-8da52b6f202444711da6b1f1baac92e0a516c8e6.tar.gz abc-8da52b6f202444711da6b1f1baac92e0a516c8e6.tar.bz2 abc-8da52b6f202444711da6b1f1baac92e0a516c8e6.zip |
Version abc70202
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 7 | ||||
-rw-r--r-- | src/base/abci/abcIvy.c | 28 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c | 3 | ||||
-rw-r--r-- | src/base/abci/abcSat.c | 6 |
4 files changed, 40 insertions, 4 deletions
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 ); |