From 5096a78fbe128785fcfff483ea6874c6b3f46836 Mon Sep 17 00:00:00 2001 From: Meneya Date: Mon, 20 Apr 2026 14:53:32 +0530 Subject: [PATCH 01/13] Added option -c to call CaDiCaL solver inside bmc3 engine (bmc3 -c) --- src/base/abci/abc.c | 6 ++- src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcBmc3.c | 74 +++++++++++++++++++++++----- src/sat/cadical/cadical.hpp | 1 + src/sat/cadical/cadicalSolver.c | 15 ++++++ src/sat/cadical/cadicalSolver.h | 1 + src/sat/cadical/cadical_ccadical.cpp | 4 ++ src/sat/cadical/cadical_solver.cpp | 4 ++ src/sat/cadical/ccadical.h | 1 + 9 files changed, 95 insertions(+), 12 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 998b3e16b..b5362ec36 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30691,7 +30691,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzhc" ) ) != EOF ) { switch ( c ) { @@ -30866,6 +30866,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': pPars->fUseGlucose ^= 1; break; + case 'c': + pPars->fUseCadical ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -30960,6 +30963,7 @@ usage: Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using Satoko by Bruno Schmitt [default = %s]\n", pPars->fUseSatoko? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere, University of Freiburg [default = %s]\n",pPars->fUseCadical? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 1e6d51a24..265c6ebc5 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -134,6 +134,7 @@ struct Saig_ParBmc_t_ int fNoRestarts; // disables periodic restarts int fUseSatoko; // enables using Satoko int fUseGlucose; // enables using Glucose 3.0 + int fUseCadical; // enables using CaDiCaL int nLearnedStart; // starting learned clause limit int nLearnedDelta; // delta of learned clause limit int nLearnedPerce; // ratio of learned clause limit diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 7e0a6cfdc..a6d5bc594 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -23,12 +23,21 @@ #include "sat/bsat/satStore.h" #include "sat/satoko/satoko.h" #include "sat/glucose/AbcGlucose.h" +#include "sat/cadical/cadicalSolver.h" +#include "sat/cadical/ccadical.h" #include "misc/vec/vecHsh.h" #include "misc/vec/vecWec.h" #include "bmc.h" ABC_NAMESPACE_IMPL_START +static inline void Bmc3_CadicalSetRuntimeLimit( cadical_solver * pSat4, abctime nSeconds ) +{ + if ( pSat4 == NULL || nSeconds <= 0 ) + return; + ccadical_limit( (CCaDiCaL *)pSat4->p, "seconds", nSeconds ); +} + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -64,6 +73,7 @@ struct Gia_ManBmc_t_ sat_solver * pSat; // SAT solver satoko_t * pSat2; // SAT solver bmcg_sat_solver * pSat3; // SAT solver + cadical_solver * pSat4; // SAT solver int nSatVars; // SAT variables int nObjNums; // SAT objects int nWordNum; // unsigned words for ternary simulation @@ -718,7 +728,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap ) SeeAlso [] ***********************************************************************/ -Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose ) +Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose, int fUseCadical ) { Gia_ManBmc_t * p; Aig_Obj_t * pObj; @@ -763,6 +773,11 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi for ( i = 0; i < 1000; i++ ) bmcg_sat_solver_addvar( p->pSat3 ); } + else if ( fUseCadical ) + { + p->pSat4 = cadical_solver_new(); + cadical_solver_setnvars(p->pSat4, 1000); + } else { p->pSat = sat_solver_new(); @@ -806,9 +821,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) p->pSat ? p->pSat->nLearntDelta : 0, p->pSat ? p->pSat->nLearntRatio : 0, p->pSat ? p->pSat->nDBreduces : 0, - p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), + p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), nUsedVars, - 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) ); + 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) ); Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n", p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps ); } @@ -830,6 +845,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) if ( p->pSat ) sat_solver_delete( p->pSat ); if ( p->pSat2 ) satoko_destroy( p->pSat2 ); if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 ); + if ( p->pSat4 ) cadical_solver_delete( p->pSat4 ); ABC_FREE( p->pTime4Outs ); Vec_IntFree( p->vData ); Hsh_IntManStop( p->vHash ); @@ -1029,6 +1045,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) ) assert( 0 ); } + else if ( p->pSat4 ) + { + if ( !cadical_solver_addclause( p->pSat4, ClaLits, ClaLits+nClaLits ) ) + assert( 0 ); + } else { if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) ) @@ -1287,6 +1308,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ ) bmcg_sat_solver_addvar( p->pSat3 ); } + else if ( p->pSat4 ) + { + for ( i = cadical_solver_nvars(p->pSat4); i < p->nSatVars; i++ ) + cadical_solver_addvar( p->pSat4 ); + } else sat_solver_setnvars( p->pSat, p->nSatVars ); return Lit; @@ -1411,6 +1437,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) ) Abc_InfoSetBit( pCex->pData, iBit + k ); } + else if ( p->pSat4) + { + if ( iLit != ~0 && cadical_solver_get_var_value(p->pSat4, lit_var(iLit)) ) + Abc_InfoSetBit( pCex->pData, iBit + k ); + } else { if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) @@ -1445,6 +1476,10 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit ) bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit ); return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 ); } + else if ( p->pSat4 ) + { + return cadical_solver_solve( p->pSat4, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + } else return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); } @@ -1482,7 +1517,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); // create BMC manager - p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose ); + p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose, pPars->fUseCadical ); p->pPars = pPars; if ( p->pSat ) { @@ -1498,6 +1533,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { // satoko_set_runid(p->pSat3, p->pPars->RunId); // satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop); + } + else if ( p->pSat4 ) + { + } else { @@ -1522,6 +1561,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop ); + else if ( p-> pSat4 ) + Bmc3_CadicalSetRuntimeLimit( p->pSat4, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1659,6 +1700,8 @@ clkOther += Abc_Clock() - clk2; satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() ); + else if ( p-> pSat4 ) + Bmc3_CadicalSetRuntimeLimit( p->pSat4, p->pTime4Outs[i] + Abc_Clock() ); else sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() ); } @@ -1690,6 +1733,8 @@ nTimeUnsat += clkSatRun; status = satoko_add_clause( p->pSat2, &Lit, 1 ); else if ( p->pSat3 ) status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 ); + else if ( p->pSat4 ) + status = cadical_solver_addclause( p->pSat4, &Lit, &Lit + 1 ); else status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); assert( status ); @@ -1721,12 +1766,12 @@ nTimeSat += clkSatRun; { Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); // ABC_PRT( "Time", Abc_Clock() - clk ); - Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); + Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) ); Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) ); Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); @@ -1773,6 +1818,8 @@ nTimeSat += clkSatRun; satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop ); + else if ( p->pSat4 ) + Bmc3_CadicalSetRuntimeLimit ( p->pSat4, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1798,6 +1845,11 @@ nTimeSat += clkSatRun; if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) continue; } + else if (p->pSat4) + { + if ( cadical_solver_get_var_value(p->pSat4, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) + continue; + } else { if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) @@ -1841,7 +1893,7 @@ nTimeUndec += clkSatRun; } if ( pPars->fVerbose ) { - if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 ) + if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 ) { fFirst = 0; // Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f ); @@ -1849,11 +1901,11 @@ nTimeUndec += clkSatRun; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); // Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); - Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); + Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); if ( pPars->fSolveAll ) Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts ); if ( pPars->nTimeOutOne ) diff --git a/src/sat/cadical/cadical.hpp b/src/sat/cadical/cadical.hpp index 7ceedcec4..4ef09e0c4 100644 --- a/src/sat/cadical/cadical.hpp +++ b/src/sat/cadical/cadical.hpp @@ -1058,6 +1058,7 @@ public: // Extra APIs int clauses (); int conflicts (); + int learned (); private: //==== start of state ==================================================== diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index f27fe19f9..30cd6c68c 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -297,6 +297,21 @@ int cadical_solver_nconflicts(cadical_solver* s) { return ccadical_conflicts((CCaDiCaL*)s->p); } +/**Function************************************************************* + + Synopsis [get number of learned clauses] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int cadical_solver_nlearned(cadical_solver* s) { + return ccadical_learned((CCaDiCaL*)s->p); +} + /**Function************************************************************* diff --git a/src/sat/cadical/cadicalSolver.h b/src/sat/cadical/cadicalSolver.h index 2aec06c2a..9e6394ff5 100644 --- a/src/sat/cadical/cadicalSolver.h +++ b/src/sat/cadical/cadicalSolver.h @@ -67,6 +67,7 @@ extern void cadical_solver_setnvars(cadical_solver* s,int n); extern int cadical_solver_get_var_value(cadical_solver* s, int v); extern int cadical_solver_nclauses(cadical_solver* s); extern int cadical_solver_nconflicts(cadical_solver* s); +extern int cadical_solver_nlearned(cadical_solver* s); extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/cadical/cadical_ccadical.cpp b/src/sat/cadical/cadical_ccadical.cpp index 3b61a0373..a929a4743 100644 --- a/src/sat/cadical/cadical_ccadical.cpp +++ b/src/sat/cadical/cadical_ccadical.cpp @@ -228,4 +228,8 @@ int ccadical_conflicts(CCaDiCaL *ptr) { return ((Wrapper *) ptr)->solver->conflicts (); } +int ccadical_learned(CCaDiCaL *ptr) { + return ((Wrapper *) ptr)->solver->learned (); +} + ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/cadical_solver.cpp b/src/sat/cadical/cadical_solver.cpp index 7dd03e8be..0efeddaa8 100644 --- a/src/sat/cadical/cadical_solver.cpp +++ b/src/sat/cadical/cadical_solver.cpp @@ -1853,6 +1853,10 @@ int Solver::conflicts () { return internal->stats.conflicts; } +int Solver::learned () { + return internal->stats.learned.clauses; +} + } // namespace CaDiCaL ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/ccadical.h b/src/sat/cadical/ccadical.h index ef442e7a3..b4401305c 100644 --- a/src/sat/cadical/ccadical.h +++ b/src/sat/cadical/ccadical.h @@ -63,6 +63,7 @@ void ccadical_resize(CCaDiCaL *, int min_max_var); int ccadical_is_inconsistent(CCaDiCaL *); int ccadical_clauses(CCaDiCaL *); int ccadical_conflicts(CCaDiCaL *); +int ccadical_learned(CCaDiCaL *); /*------------------------------------------------------------------------*/ From 26567123a74d97c95d060c4f17a548cfd2eefde4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 15 May 2026 17:47:46 -0700 Subject: [PATCH 02/13] Fix warnings. --- src/base/abci/abc.c | 8 ++++---- src/opt/eslim/relationSynthesiser.cpp | 6 +++--- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1167511d5..d706487ec 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51736,12 +51736,12 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &sprove [-PTUW num] [-C str] [-R file] [-usvwh]\n" ); - Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); + Abc_Print( -2, "\t concurrent sequential model checker\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs ); - Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); - Abc_Print( -2, "\t-U num : second-stage timeout in seconds [default = %d]\n", nTimeOut2 ); + Abc_Print( -2, "\t-T num : first-stage timeout for proving original and scnew reduction [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-U num : second-stage proving timeout on optimized miter [default = %d]\n", nTimeOut2 ); + Abc_Print( -2, "\t-W num : late-stage timeout for optimization and final proving [default = %d]\n", nTimeOut3 ); Abc_Print( -2, "\t-C str : with -u, pass this option string to internal %%ufar\n" ); - Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" ); Abc_Print( -2, "\t-u : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" ); Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" ); diff --git a/src/opt/eslim/relationSynthesiser.cpp b/src/opt/eslim/relationSynthesiser.cpp index 6e639fc04..70a488d83 100644 --- a/src/opt/eslim/relationSynthesiser.cpp +++ b/src/opt/eslim/relationSynthesiser.cpp @@ -27,8 +27,8 @@ ABC_NAMESPACE_IMPL_START namespace eSLIM { RelationSynthesiser::RelationSynthesiser(const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log) - : relation(relation), subcir(subcir), - max_size(max_size), config(cfg), log(log) { + : subcir(subcir), max_size(max_size), + relation(relation), config(cfg), log(log) { setupEncoding(); } @@ -609,4 +609,4 @@ namespace eSLIM { } -ABC_NAMESPACE_IMPL_END \ No newline at end of file +ABC_NAMESPACE_IMPL_END From 7bf1177d3900212df9e5c32ffc3ff2f59bc9b02b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 15 May 2026 17:57:45 -0700 Subject: [PATCH 03/13] Add MM-based adder generation to &genadder. --- src/aig/gia/giaGen.c | 103 ++++++++++++++++++++++++++++++++++++++----- src/base/abci/abc.c | 14 +++--- 2 files changed, 100 insertions(+), 17 deletions(-) diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c index 426409c70..edd3a28af 100644 --- a/src/aig/gia/giaGen.c +++ b/src/aig/gia/giaGen.c @@ -1446,23 +1446,76 @@ void Gia_ManGenPrefix( Gia_Man_t * pNew, int * p, int * g, int p2, int g2 ) *g = Gia_ManHashOr(pNew, *g, Gia_ManHashAnd(pNew, *p, g2)); *p = Gia_ManHashAnd(pNew, *p, p2); } -Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose ) +static int Gia_ManGenAdderMaj( Gia_Man_t * p, int a, int b, int c ) +{ + int ab = Gia_ManHashAnd( p, a, b ); + int ac = Gia_ManHashAnd( p, a, c ); + int bc = Gia_ManHashAnd( p, b, c ); + return Gia_ManHashOr( p, ab, Gia_ManHashOr( p, ac, bc ) ); +} +static int Gia_ManGenAdderFloorPow2( int n ) +{ + int r = 1; + assert( n > 0 ); + while ( r <= n / 2 ) + r *= 2; + return r; +} +static void Gia_ManGenAdderMMRange( Gia_Man_t * p, int nVars, int * pLitsI, int * pM0, int * pM1, int i, int k ) +{ + int Index = i * nVars + k; + int nRange, nLeft, j; + assert( 0 <= i && i <= k && k < nVars ); + if ( pM0[Index] >= 0 ) + return; + if ( i == k ) + { + pM0[Index] = pLitsI[2*i]; + pM1[Index] = pLitsI[2*i+1]; + return; + } + nRange = k - i + 1; + nLeft = Gia_ManGenAdderFloorPow2( nRange - 1 ); + j = i + nLeft - 1; + Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, i, j ); + Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, j+1, k ); + pM0[Index] = Gia_ManGenAdderMaj( p, pM0[(j+1)*nVars+k], pM1[(j+1)*nVars+k], pM0[i*nVars+j] ); + pM1[Index] = Gia_ManGenAdderMaj( p, pM0[(j+1)*nVars+k], pM1[(j+1)*nVars+k], pM1[i*nVars+j] ); +} +static int Gia_ManGenAdderMMCarry( Gia_Man_t * p, int nVars, int * pLitsI, int * pM0, int * pM1, int * pCarries, int iCarry ) +{ + int nBase, iBeg; + assert( 0 <= iCarry && iCarry <= nVars ); + if ( pCarries[iCarry] >= 0 ) + return pCarries[iCarry]; + nBase = Gia_ManGenAdderFloorPow2( iCarry ); + iBeg = nBase - 1; + Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, iBeg, iCarry-1 ); + pCarries[iCarry] = Gia_ManGenAdderMaj( p, pM0[iBeg*nVars+iCarry-1], pM1[iBeg*nVars+iCarry-1], Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, iBeg ) ); + return pCarries[iCarry]; +} +Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int fCarries, int fVerbose ) { extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps ); int i, k, nBits = Abc_Base2Log(nVars), nVarsAlloc = (1 << nBits) + 2; - int ** pStore = (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 ); + int ** pStore = fMM ? NULL : (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 ); printf( "Generating %d-bit ", nVars ); - Gia_ManGenPrep( nVars+2, pStore ); - if ( fSK ) - Gia_ManGenSK( nVars, pStore ), printf("Sklansky "); - else if ( fBK ) - Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung "); - else if ( fHC ) - Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson "); + if ( fMM ) + printf("M/M "); else - Gia_ManGenRca( nVars, pStore ), printf("ripple-carry "); + { + Gia_ManGenPrep( nVars+2, pStore ); + if ( fSK ) + Gia_ManGenSK( nVars, pStore ), printf("Sklansky "); + else if ( fBK ) + Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung "); + else if ( fHC ) + Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson "); + else + Gia_ManGenRca( nVars, pStore ), printf("ripple-carry "); + } printf( "adder with%s carry-in and carry-out\n", fCarries ? "":"out" ); - if ( fVerbose ) Gia_ManGenPrint( nVars, pStore ); + if ( fVerbose && !fMM ) Gia_ManGenPrint( nVars, pStore ); Gia_Man_t * p = Gia_ManStart( 1000 ), * pTemp; p->pName = Abc_UtilStrsav( "adder" ); int * pLitsI = ABC_CALLOC( int, 2*nVars+10 ); @@ -1472,6 +1525,33 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, pLitsI[2*k+1] = Gia_ManAppendCi(p); int Carry = fCarries ? Gia_ManAppendCi(p) : 0; Gia_ManHashStart( p ); + if ( fMM ) + { + int nPairs = nVars * nVars; + int * pM0 = ABC_ALLOC( int, nPairs ); + int * pM1 = ABC_ALLOC( int, nPairs ); + int * pCarries = ABC_ALLOC( int, nVars + 1 ); + int * pProps = ABC_ALLOC( int, nVars ); + for ( k = 0; k < nPairs; k++ ) + pM0[k] = pM1[k] = -1; + for ( k = 0; k <= nVars; k++ ) + pCarries[k] = -1; + pCarries[0] = Carry; + for ( k = 0; k < nVars; k++ ) + pProps[k] = Gia_ManHashXor( p, pLitsI[2*k], pLitsI[2*k+1] ); + if ( fCarries ) + Gia_ManAppendCo( p, Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, nVars ) ); + for ( k = 0; k < nVars; k++ ) + Gia_ManAppendCo( p, Gia_ManHashXor( p, pProps[k], Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, k ) ) ); + ABC_FREE( pM0 ); + ABC_FREE( pM1 ); + ABC_FREE( pCarries ); + ABC_FREE( pProps ); + ABC_FREE( pLitsI ); + p = Gia_ManCleanup( pTemp = p ); + Gia_ManStop( pTemp ); + return p; + } for ( k = 0; k < nVars; k++ ) Wlc_BlastFullAdder( p, pLitsI[2*k], pLitsI[2*k+1], k ? 0 : Carry, &pLitsI[2*k+1], &pLitsI[2*k] ); int * pLits = ABC_CALLOC( int, 2*nVars+10 ); @@ -1498,4 +1578,3 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d706487ec..7b34b3d62 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -58734,11 +58734,11 @@ usage: ***********************************************************************/ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose ); + extern Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int fCarries, int fVerbose ); Gia_Man_t * pTemp = NULL; - int c, nBits = 0, fSK = 0, fBK = 0, fHC = 0, fCarries = 0, fVerbose = 0; + int c, nBits = 0, fSK = 0, fBK = 0, fHC = 0, fMM = 0, fCarries = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nsbhcv" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nsbhmcv" ) ) != EOF ) { switch ( c ) { @@ -58762,6 +58762,9 @@ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'h': fHC ^= 1; break; + case 'm': + fMM ^= 1; + break; case 'c': fCarries ^= 1; break; @@ -58777,17 +58780,18 @@ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9GenAdder(): The number of inputs should be defined on the command line \"-N num\".\n" ); return 0; } - pTemp = Gia_ManGenAdder( nBits, fSK, fBK, fHC, fCarries, fVerbose ); + pTemp = Gia_ManGenAdder( nBits, fSK, fBK, fHC, fMM, fCarries, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &genadder [-N ] [-sbhcv]\n" ); + Abc_Print( -2, "usage: &genadder [-N ] [-sbhmcv]\n" ); Abc_Print( -2, "\t generates a prefix adder (by default, the ripple carry adder)\n" ); Abc_Print( -2, "\t-N num : the bit-width of the adder [default = undefined]\n" ); Abc_Print( -2, "\t-s : toggles using Sklansky adder [default = %s]\n", fSK ? "yes": "no" ); Abc_Print( -2, "\t-b : toggles using Brent-Kung adder [default = %s]\n", fBK ? "yes": "no" ); Abc_Print( -2, "\t-h : toggles using Huan-Carlsson adder [default = %s]\n", fHC ? "yes": "no" ); + Abc_Print( -2, "\t-m : toggles using majority-based M/M adder [default = %s]\n", fMM ? "yes": "no" ); Abc_Print( -2, "\t-c : toggles using carry-in and carry-out [default = %s]\n", fCarries ? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); return 1; From 07e38ef030bf70f9952491be68b5ef9e6e65ab8e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 17 May 2026 18:51:49 -0700 Subject: [PATCH 04/13] Imrpovements in "twoexact". --- src/base/abci/abc.c | 544 +++++++++++++++++++++++++++++++++++++++++- src/sat/bmc/bmc.h | 2 + src/sat/bmc/bmcMaj.c | 163 +++++++++++-- src/sat/bmc/bmcMaj2.c | 152 +++++++++++- 4 files changed, 823 insertions(+), 38 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7b34b3d62..c84663fd9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10602,19 +10602,356 @@ usage: SeeAlso [] ***********************************************************************/ +static int Abc_TwoExactPermAddFanin( int * pFans, int iNode, int iFanin ) +{ + int * pNode = pFans + 2 * iNode; + if ( pNode[0] == iFanin || pNode[1] == iFanin ) + return 0; + if ( pNode[0] == -1 && pNode[1] == -1 ) + pNode[Abc_Random(0) & 1] = iFanin; + else if ( pNode[0] == -1 ) + pNode[0] = iFanin; + else if ( pNode[1] == -1 ) + pNode[1] = iFanin; + else + return 0; + return 1; +} +static int Abc_TwoExactPermAddRequired( int * pFans, int nVars, int nNodes, int iFanin ) +{ + int iNodeStart = (iFanin + 1 > nVars) ? iFanin + 1 - nVars : 0; + int i, nChoices = 0, iChoice = -1; + for ( i = iNodeStart; i < nNodes; i++ ) + { + int * pNode = pFans + 2 * i; + if ( pNode[0] == iFanin || pNode[1] == iFanin ) + continue; + if ( pNode[0] != -1 && pNode[1] != -1 ) + continue; + if ( Abc_Random(0) % ++nChoices == 0 ) + iChoice = i; + } + return iChoice >= 0 && Abc_TwoExactPermAddFanin( pFans, iChoice, iFanin ); +} +static int Abc_TwoExactPermCountDistinct( int * pFans, int nVars, int iNode ) +{ + int iPrevObj = nVars + iNode - 1; + int pVals[4], nVals = 0, i, k; + assert( iNode > 0 ); + for ( i = iNode - 1; i <= iNode; i++ ) + for ( k = 0; k < 2; k++ ) + { + int v = pFans[2 * i + k]; + int j, fSeen = 0; + if ( v == iPrevObj ) + continue; + for ( j = 0; j < nVals; j++ ) + fSeen |= pVals[j] == v; + if ( !fSeen ) + pVals[nVals++] = v; + } + return nVals; +} +static int Abc_TwoExactPermCheck( int * pFans, int nVars, int nNodes, int fStrict ) +{ + int nObjs = nVars + nNodes; + int * pUsed = ABC_CALLOC( int, nObjs ); + int i, RetValue = 1; + for ( i = 0; i < nNodes; i++ ) + { + if ( pFans[2*i] < 0 || pFans[2*i+1] < 0 || pFans[2*i] >= nVars + i || pFans[2*i+1] >= nVars + i || pFans[2*i] == pFans[2*i+1] ) + RetValue = 0; + if ( fStrict && i > 0 && Abc_TwoExactPermCountDistinct(pFans, nVars, i) < 3 ) + RetValue = 0; + if ( !RetValue ) + break; + pUsed[pFans[2*i]]++; + pUsed[pFans[2*i+1]]++; + } + if ( RetValue ) + for ( i = 0; i < nObjs - 1; i++ ) + if ( pUsed[i] == 0 ) + { + RetValue = 0; + break; + } + ABC_FREE( pUsed ); + return RetValue; +} +static char * Abc_TwoExactPermEncode( int * pFans, int nVars, int nNodes ) +{ + char * pPerm = ABC_ALLOC( char, 3 * nNodes ); + int i, k, Pos = 0; + for ( i = 0; i < nNodes; i++ ) + { + if ( i ) + pPerm[Pos++] = '_'; + for ( k = 0; k < 2; k++ ) + pPerm[Pos++] = pFans[2*i+k] >= 0 && pFans[2*i+k] < nVars ? 'a' + pFans[2*i+k] : '*'; + } + pPerm[Pos] = 0; + return pPerm; +} +static char * Abc_TwoExactObjName( int iObj, int nVars, char * pBuffer ) +{ + if ( iObj < 0 ) + sprintf( pBuffer, "*" ); + else if ( iObj < nVars ) + sprintf( pBuffer, "%c", 'a' + iObj ); + else if ( iObj - nVars < 26 ) + sprintf( pBuffer, "%c", 'A' + iObj - nVars ); + else + sprintf( pBuffer, "N%d", iObj - nVars ); + return pBuffer; +} +static char * Abc_TwoExactPermEncodeFull( int * pFans, int nVars, int nNodes ) +{ + int nSize = 8 * (nNodes + 1); + char * pPerm = ABC_ALLOC( char, nSize ); + int i, k, Pos = 0; + char Name[16]; + for ( i = 0; i < nNodes; i++ ) + { + if ( i ) + pPerm[Pos++] = '_'; + for ( k = 0; k < 2; k++ ) + Pos += sprintf( pPerm + Pos, "%s", Abc_TwoExactObjName(pFans[2*i+k], nVars, Name) ); + } + pPerm[Pos] = 0; + return pPerm; +} +static int Abc_TwoExactPermAddDcs( int * pFans, int nVars, int nNodes, int nDcs, int nSkip, int fAll ) +{ + int i, k, nLetters = 0; + if ( nDcs == 0 ) + return 1; + for ( i = nSkip; i < 2 * nNodes; i++ ) + nLetters += pFans[i] >= 0 && (fAll || pFans[i] < nVars); + if ( nDcs > nLetters ) + return 0; + for ( k = 0; k < nDcs; k++ ) + { + int iChoice = -1, nChoices = 0; + for ( i = nSkip; i < 2 * nNodes; i++ ) + if ( pFans[i] >= 0 && (fAll || pFans[i] < nVars) && Abc_Random(0) % ++nChoices == 0 ) + iChoice = i; + assert( iChoice >= 0 ); + pFans[iChoice] = -1; + } + return 1; +} +static int * Abc_TwoExactPermRandom( int nVars, int nNodes, int nDcs ) +{ + int nObjs = nVars + nNodes; + int Attempt, i, k; + for ( Attempt = 0; Attempt < 200; Attempt++ ) + { + int * pFans = ABC_ALLOC( int, 2 * nNodes ); + int fOk = 1; + for ( i = 0; i < 2 * nNodes; i++ ) + pFans[i] = -1; + for ( i = nObjs - 2; i >= nVars && fOk; i-- ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nVars && fOk; i++ ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nNodes && fOk; i++ ) + { + int Limit = nVars + i; + for ( k = 0; k < 2; k++ ) + { + int Try; + if ( pFans[2*i+k] != -1 ) + continue; + for ( Try = 0; Try < 100; Try++ ) + if ( Abc_TwoExactPermAddFanin( pFans, i, Abc_Random(0) % Limit ) ) + break; + if ( Try == 100 ) + fOk = 0; + } + if ( pFans[2*i] > pFans[2*i+1] ) + ABC_SWAP( int, pFans[2*i], pFans[2*i+1] ); + } + if ( fOk && Abc_TwoExactPermCheck(pFans, nVars, nNodes, 1) && Abc_TwoExactPermAddDcs(pFans, nVars, nNodes, nDcs, 0, 0) ) + return pFans; + ABC_FREE( pFans ); + } + return NULL; +} +static int * Abc_TwoExactPermRandomSeeded( int nVars, int nNodes, int nDcs, Vec_Int_t * vSeedPairs, int nSeeds ) +{ + int nObjs = nVars + nNodes; + int Attempt, i, k; + nSeeds = Abc_MinInt( nSeeds, Vec_IntSize(vSeedPairs) ); + for ( Attempt = 0; Attempt < 200; Attempt++ ) + { + int * pFans = ABC_ALLOC( int, 2 * nNodes ); + int * pUsed = ABC_CALLOC( int, Vec_IntSize(vSeedPairs) ); + int fOk = 1; + for ( i = 0; i < 2 * nNodes; i++ ) + pFans[i] = -1; + for ( i = 0; i < nSeeds; i++ ) + { + int s, iSeed = -1, nChoices = 0; + for ( s = 0; s < Vec_IntSize(vSeedPairs); s++ ) + if ( !pUsed[s] && Abc_Random(0) % ++nChoices == 0 ) + iSeed = s; + assert( iSeed >= 0 ); + pUsed[iSeed] = 1; + int Pair = Vec_IntEntry( vSeedPairs, iSeed ); + pFans[2*i] = Pair / nVars; + pFans[2*i+1] = Pair % nVars; + } + for ( i = nObjs - 2; i >= nVars && fOk; i-- ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nVars && fOk; i++ ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nNodes && fOk; i++ ) + { + int Limit = nVars + i; + for ( k = 0; k < 2; k++ ) + { + int Try; + if ( pFans[2*i+k] != -1 ) + continue; + for ( Try = 0; Try < 100; Try++ ) + if ( Abc_TwoExactPermAddFanin( pFans, i, Abc_Random(0) % Limit ) ) + break; + if ( Try == 100 ) + fOk = 0; + } + if ( pFans[2*i] > pFans[2*i+1] ) + ABC_SWAP( int, pFans[2*i], pFans[2*i+1] ); + } + if ( fOk && Abc_TwoExactPermCheck(pFans, nVars, nNodes, 0) && Abc_TwoExactPermAddDcs(pFans, nVars, nNodes, nDcs, 2*nSeeds, 1) ) + { + ABC_FREE( pUsed ); + return pFans; + } + ABC_FREE( pUsed ); + ABC_FREE( pFans ); + } + return NULL; +} +static char * Abc_TwoExactCofactorHex( char * pHex, int nVars, int iVar, int Value ) +{ + word pTruth[64], pCof[64]; + int nCofVars = nVars - 1; + int nMints = 1 << nCofVars; + char * pRes = ABC_ALLOC( char, (nCofVars >= 2 ? (1 << (nCofVars-2)) : 1) + 10 ); + int m; + memset( pTruth, 0, sizeof(word) * 64 ); + memset( pCof, 0, sizeof(word) * 64 ); + Abc_TtReadHex( pTruth, pHex ); + for ( m = 0; m < nMints; m++ ) + { + int Low = m & ((1 << iVar) - 1); + int High = m >> iVar; + int Mint = Low | (Value << iVar) | (High << (iVar + 1)); + if ( Abc_TtGetBit(pTruth, Mint) ) + Abc_TtSetBit( pCof, m ); + } + Extra_PrintHexadecimalString( pRes, (unsigned *)pCof, nCofVars ); + return pRes; +} +static int Abc_TwoExactRun( Bmc_EsPar_t * pPars ) +{ + extern int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + return pPars->fGlucose ? Exa_ManExactSynthesis( pPars ) : Exa_ManExactSynthesis2( pPars ); +} +static int Abc_TwoExactRunMin( Bmc_EsPar_t * pPars, int nNodeMax ) +{ + int n, nNodeBeg = pPars->nVars + 1; + int fFound = 0; + for ( n = nNodeBeg; n <= nNodeMax; n++ ) + { + if ( !pPars->fSilent ) + printf( "\nTrying N = %d:\n", n ); + pPars->nNodes = n; + ABC_FREE( pPars->pSolFans ); + fFound = Abc_TwoExactRun( pPars ); + if ( fFound ) + return n; + } + return 0; +} +static Vec_Int_t * Abc_TwoExactCofactorSeeds( Bmc_EsPar_t * pPars, int nNodeMax ) +{ + int Counts[16][16]; + int v, c, i, k, nPairs = 0; + Vec_Int_t * vPairs = Vec_IntAlloc( 16 ); + memset( Counts, 0, sizeof(Counts) ); + if ( pPars->nVars > 16 ) + return vPairs; + for ( v = 0; v < pPars->nVars; v++ ) + for ( c = 0; c < 2; c++ ) + { + Bmc_EsPar_t CofPars, * pCof = &CofPars; + char * pCofHex = Abc_TwoExactCofactorHex( pPars->pTtStr, pPars->nVars, v, c ); + int nFound; + Bmc_EsParSetDefault( pCof ); + pCof->nVars = pPars->nVars - 1; + pCof->nNodes = nNodeMax; + pCof->pTtStr = pCofHex; + pCof->fOnlyAnd = pPars->fOnlyAnd; + pCof->fGlucose = pPars->fGlucose; + pCof->RuntimeLim = pPars->RuntimeLim ? pPars->RuntimeLim : 1; + pCof->fSilent = 1; + nFound = Abc_TwoExactRunMin( pCof, nNodeMax ); + if ( nFound ) + { + printf( "Cofactor %c=%d: minimum N = %d, truth = %s\n", 'a' + v, c, nFound, pCofHex ); + for ( i = 0; i < nFound; i++ ) + { + int Fan0 = pCof->pSolFans[2*i]; + int Fan1 = pCof->pSolFans[2*i+1]; + if ( Fan0 >= pCof->nVars || Fan1 >= pCof->nVars ) + continue; + Fan0 += Fan0 >= v; + Fan1 += Fan1 >= v; + if ( Fan0 > Fan1 ) + ABC_SWAP( int, Fan0, Fan1 ); + Counts[Fan0][Fan1]++; + } + } + else + printf( "Cofactor %c=%d: no solution up to N = %d, truth = %s\n", 'a' + v, c, nNodeMax, pCofHex ); + ABC_FREE( pCof->pSolFans ); + ABC_FREE( pCofHex ); + } + for ( k = pPars->nVars * pPars->nVars; k > 0; k-- ) + { + int BestI = -1, BestJ = -1, Best = 0; + for ( i = 0; i < pPars->nVars; i++ ) + for ( v = i + 1; v < pPars->nVars; v++ ) + if ( Counts[i][v] > Best ) + { + Best = Counts[i][v]; + BestI = i; + BestJ = v; + } + if ( Best == 0 ) + break; + printf( "Frequent seed %d: %c%c appears %d time%s.\n", ++nPairs, 'a' + BestI, 'a' + BestJ, Best, Best == 1 ? "" : "s" ); + for ( v = 0; v < Best; v++ ) + Vec_IntPush( vPairs, BestI * pPars->nVars + BestJ ); + Counts[BestI][BestJ] = 0; + } + return vPairs; +} int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); - extern void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + extern int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName ); extern void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ); - int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0; + int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0, nCandPerms = 0, nPermDcs = 0, fTryMin = 0, fSmartGen = 0, nSeedNodes = 0; Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSabdconugklmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSPCDEabdconugklmtxvh" ) ) != EOF ) { switch ( c ) { @@ -10671,6 +11008,48 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pGuide = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a variable permutation.\n" ); + goto usage; + } + pPars->pPermStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nCandPerms = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCandPerms < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nPermDcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPermDcs < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" ); + goto usage; + } + nSeedNodes = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSeedNodes < 0 ) + goto usage; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -10704,6 +11083,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fCard ^= 1; break; + case 't': + fTryMin ^= 1; + break; + case 'x': + fSmartGen ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -10717,6 +11102,11 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( strstr(argv[globalUtilOptind], ".") ) { + if ( pPars->pPermStr || nCandPerms ) + { + Abc_Print( -1, "Permutation options -P and -C are not supported when reading the function from a file.\n" ); + return 1; + } Exa_ManExactSynthesis6( pPars, argv[globalUtilOptind] ); return 0; } @@ -10742,6 +11132,143 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Function should not have more than 10 inputs.\n" ); return 1; } + if ( nPermDcs && nCandPerms == 0 ) + { + Abc_Print( -1, "Command line switch \"-D\" can only be used together with \"-C\".\n" ); + return 1; + } + if ( fSmartGen && nCandPerms == 0 ) + { + Abc_Print( -1, "Command line switch \"-x\" can only be used together with \"-C\".\n" ); + return 1; + } + if ( nSeedNodes && !fSmartGen ) + { + Abc_Print( -1, "Command line switch \"-E\" can only be used together with \"-x\".\n" ); + return 1; + } + if ( nCandPerms && pPars->pPermStr ) + { + Abc_Print( -1, "Command line switch \"-C\" cannot be used together with \"-P\".\n" ); + return 1; + } + if ( fTryMin && nCandPerms ) + { + Abc_Print( -1, "Command line switch \"-t\" cannot be used together with \"-C\".\n" ); + return 1; + } + if ( nPermDcs > 2 * pPars->nNodes ) + { + Abc_Print( -1, "The number of don't-care positions should not exceed %d.\n", 2 * pPars->nNodes ); + return 1; + } + if ( pPars->pPermStr ) + { + int i, nEntries = 0; + for ( i = 0; pPars->pPermStr[i]; i++ ) + { + char Sym = pPars->pPermStr[i]; + if ( Sym == '_' ) + continue; + if ( Sym != '*' && (Sym < 'a' || Sym >= 'a' + pPars->nVars) ) + { + Abc_Print( -1, "Permutation symbol \"%c\" is not one of '*', '_' or input variables 'a' through '%c'.\n", Sym, 'a' + pPars->nVars - 1 ); + return 1; + } + nEntries++; + } + if ( nEntries != 2 * pPars->nNodes ) + { + Abc_Print( -1, "Permutation should contain %d non-separator symbols (instead of %d).\n", 2 * pPars->nNodes, nEntries ); + return 1; + } + if ( fUseNands || fKissat || fKissat2 || pPars->fCard ) + { + Abc_Print( -1, "Permutation option -P is currently supported by the default and Glucose (-g) twoexact engines.\n" ); + return 1; + } + } + if ( nCandPerms ) + { + int i, fFound = 0, nGenerated = 0, nFailed = 0, fSilentSave = pPars->fSilent; + Vec_Int_t * vSeedPairs = NULL; + abctime clk = Abc_Clock(); + if ( fUseNands || fKissat || fKissat2 || pPars->fCard ) + { + Abc_Print( -1, "Candidate generation with -C is currently supported by the default and Glucose (-g) twoexact engines.\n" ); + return 1; + } + Abc_Random( 1 ); + if ( fSmartGen ) + { + printf( "Deriving frequent seed nodes from cofactors.\n" ); + vSeedPairs = Abc_TwoExactCofactorSeeds( pPars, pPars->nNodes ); + nSeedNodes = Abc_MinInt( nSeedNodes, Vec_IntSize(vSeedPairs) ); + printf( "Trying %d smart candidate input assignments with %d frozen seed node%s and %d randomized don't-care position%s.\n", nCandPerms, nSeedNodes, nSeedNodes == 1 ? "" : "s", nPermDcs, nPermDcs == 1 ? "" : "s" ); + } + else + printf( "Trying %d random candidate input assignments with %d randomized don't-care position%s.\n", nCandPerms, nPermDcs, nPermDcs == 1 ? "" : "s" ); + pPars->fSilent = 1; + for ( i = 0; i < nCandPerms; i++ ) + { + int * pFans = fSmartGen ? Abc_TwoExactPermRandomSeeded( pPars->nVars, pPars->nNodes, nPermDcs, vSeedPairs, nSeedNodes ) : Abc_TwoExactPermRandom( pPars->nVars, pPars->nNodes, nPermDcs ); + char * pPerm, * pStruct; + if ( pFans == NULL ) + { + nFailed++; + continue; + } + pPerm = Abc_TwoExactPermEncode( pFans, pPars->nVars, pPars->nNodes ); + pStruct = Abc_TwoExactPermEncodeFull( pFans, pPars->nVars, pPars->nNodes ); + nGenerated++; + pPars->pPermFans = pFans; + pPars->pPermStr = pPerm; + if ( nGenerated == 1 || nGenerated % 10000 == 0 ) + printf( "Trying candidate %d/%d: %s\n", nGenerated, nCandPerms, pStruct ); + fFound = pPars->fGlucose ? Exa_ManExactSynthesis( pPars ) : Exa_ManExactSynthesis2( pPars ); + if ( fFound ) + { + pPars->fSilent = fSilentSave; + Abc_TwoExactRun( pPars ); + printf( "Found solution using candidate %d: %s\n", nGenerated, pStruct ); + ABC_FREE( pStruct ); + ABC_FREE( pPerm ); + ABC_FREE( pFans ); + break; + } + ABC_FREE( pStruct ); + ABC_FREE( pPerm ); + ABC_FREE( pFans ); + pPars->pPermStr = NULL; + pPars->pPermFans = NULL; + } + pPars->pPermStr = NULL; + pPars->pPermFans = NULL; + pPars->fSilent = fSilentSave; + Vec_IntFreeP( &vSeedPairs ); + ABC_FREE( pPars->pSolFans ); + if ( !fFound ) + printf( "No solution found after trying %d generated candidate%s (%d generation failure%s).\n", nGenerated, nGenerated == 1 ? "" : "s", nFailed, nFailed == 1 ? "" : "s" ); + Abc_PrintTime( 1, "Total candidate-search runtime", Abc_Clock() - clk ); + return 0; + } + if ( fTryMin ) + { + if ( fUseNands || fKissat || fKissat2 || pPars->fCard ) + { + Abc_Print( -1, "Minimum-node enumeration with -t is currently supported by the default and Glucose (-g) twoexact engines.\n" ); + return 1; + } + if ( pPars->nNodes < pPars->nVars + 1 ) + { + Abc_Print( -1, "Command line switch \"-t\" expects \"-N \" to be at least %d.\n", pPars->nVars + 1 ); + return 1; + } + if ( !Abc_TwoExactRunMin(pPars, pPars->nNodes) ) + printf( "No solution found from N = %d through N = %d.\n", pPars->nVars + 1, pPars->nNodes ); + ABC_FREE( pPars->pSolFans ); + return 0; + } if ( fUseNands ) Exa_ManExactSynthesis7( pPars, GateSize ); else if ( fKissat || pPars->fCard ) @@ -10752,16 +11279,21 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Exa_ManExactSynthesis( pPars ); else Exa_ManExactSynthesis2( pPars ); + ABC_FREE( pPars->pSolFans ); return 0; usage: - Abc_Print( -2, "usage: twoexact [-INTG ] [-S str] [-abdconugklmvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTGCDE ] [-S str] [-P str] [-abdconugklmtxvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of two-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-G : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize ); Abc_Print( -2, "\t-S : structural guidance from the user [default = %s]\n", pPars->pGuide ? pPars->pGuide : "unknown" ); + Abc_Print( -2, "\t-P : fixed input permutation; '_' separates gates, '*' leaves fanin free [default = %s]\n", pPars->pPermStr ? pPars->pPermStr : "none" ); + Abc_Print( -2, "\t-C : number of random candidate permutations to try [default = %d]\n", nCandPerms ); + Abc_Print( -2, "\t-D : number of fixed variable positions randomized to '*' in each candidate [default = %d]\n", nPermDcs ); + Abc_Print( -2, "\t-E : number of frequent cofactor seed nodes used with -x [default = %d]\n", nSeedNodes ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" ); Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" ); @@ -10773,6 +11305,8 @@ usage: Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" ); Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" ); Abc_Print( -2, "\t-m : toggle using CaDiCaL by Armin Biere [default = %s]\n", pPars->fCard ? "yes" : "no" ); + Abc_Print( -2, "\t-t : toggle trying increasing node counts up to \"-N \" [default = %s]\n", fTryMin ? "yes" : "no" ); + Abc_Print( -2, "\t-x : toggle smart candidate generation using cofactor seed nodes [default = %s]\n", fSmartGen ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : truth table in hex notation\n" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 265c6ebc5..83ddc810a 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -82,6 +82,8 @@ struct Bmc_EsPar_t_ char * pSymStr; char * pPermStr; char * pGuide; + int * pPermFans; + int * pSolFans; Vec_Wrd_t* vTruths; }; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index e342ff350..eadcd08ad 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -488,7 +488,8 @@ int Exa_ManMarkup( Exa_Man_t * p ) } } } - printf( "The number of parameter variables = %d.\n", p->iVar ); + if ( !p->pPars->fSilent ) + printf( "The number of parameter variables = %d.\n", p->iVar ); return p->iVar; // printout for ( i = p->nVars; i < p->nObjs; i++ ) @@ -569,6 +570,18 @@ static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k ) assert( Count == 1 ); return iVar; } +static inline char * Exa_ManObjName( Exa_Man_t * p, int iObj, char * pBuffer ) +{ + if ( iObj < 0 ) + sprintf( pBuffer, "*" ); + else if ( iObj < p->nVars ) + sprintf( pBuffer, "%c", 'a' + iObj ); + else if ( iObj - p->nVars < 26 ) + sprintf( pBuffer, "%c", 'A' + iObj - p->nVars ); + else + sprintf( pBuffer, "N%d", iObj - p->nVars ); + return pBuffer; +} static inline int Exa_ManEval( Exa_Man_t * p ) { static int Flag = 0; @@ -637,20 +650,18 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl ) int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart); int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1); int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2); + char Name[16]; fprintf( pFile, ".names" ); for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - if ( iVar >= 0 && iVar < p->nVars ) - fprintf( pFile, " %c", 'a'+iVar ); - else - fprintf( pFile, " %02d", iVar ); + fprintf( pFile, " %s", Exa_ManObjName(p, iVar, Name) ); } if ( i == p->nObjs - 1 ) fprintf( pFile, " F\n" ); else - fprintf( pFile, " %02d\n", i ); + fprintf( pFile, " %s\n", Exa_ManObjName(p, i, Name) ); if ( i == p->nObjs - 1 && fCompl ) fprintf( pFile, "00 1\n" ); if ( (i == p->nObjs - 1 && fCompl) ^ Val1 ) @@ -668,6 +679,7 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl ) void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) { int i, k, iVar; + char Name[16]; printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes ); // for ( i = p->nVars + 2; i < p->nObjs; i++ ) for ( i = p->nObjs - 1; i >= p->nVars; i-- ) @@ -677,20 +689,80 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1); int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2); if ( i == p->nObjs - 1 && fCompl ) - printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 ); + printf( "%s = 4\'b%d%d%d1(", Exa_ManObjName(p, i, Name), !Val3, !Val2, !Val1 ); else - printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 ); + printf( "%s = 4\'b%d%d%d0(", Exa_ManObjName(p, i, Name), Val3, Val2, Val1 ); for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - if ( iVar >= 0 && iVar < p->nVars ) - printf( " %c", 'a'+iVar ); - else - printf( " %02d", iVar ); + printf( " %s", Exa_ManObjName(p, iVar, Name) ); } printf( " )\n" ); } } +static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k ) +{ + char * pPermStr = p->pPars->pPermStr; + int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1); + int nSeen = 0, s; + if ( p->pPars->pPermFans ) + return p->pPars->pPermFans[iTarget]; + assert( pPermStr != NULL ); + for ( s = 0; pPermStr[s]; s++ ) + { + if ( pPermStr[s] == '_' ) + continue; + if ( nSeen++ == iTarget ) + return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a'; + } + assert( 0 ); + return -1; +} +static void Exa_ManPrintPermFanin( Exa_Man_t * p, int iFanin ) +{ + char Name[16]; + printf( "%s ", Exa_ManObjName(p, iFanin, Name) ); +} +static void Exa_ManPrintFixedPerm( Exa_Man_t * p ) +{ + int i, k; + char Name[16]; + if ( (p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL) || p->pPars->fSilent ) + return; + printf( "Using fixed input assignment provided by the user %s:\n", p->pPars->pPermStr ? p->pPars->pPermStr : "" ); + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) + { + printf( "%s : ", Exa_ManObjName(p, i, Name) ); + for ( k = 1; k >= 0; k-- ) + Exa_ManPrintPermFanin( p, Exa_ManPermFanin(p, i, k) ); + printf( "\n" ); + } +} +static void Exa_ManPrintPerm( Exa_Man_t * p ) +{ + int i, k, iVar; + printf( "The variable permutation is \"" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + if ( i > p->nVars ) + printf( "_" ); + for ( k = 1; k >= 0; k-- ) + { + iVar = Exa_ManFindFanin( p, i, k ); + printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' ); + } + } + printf( "\".\n" ); +} +static void Exa_ManSaveSolution( Exa_Man_t * p ) +{ + int i, k, Pos = 0; + ABC_FREE( p->pPars->pSolFans ); + p->pPars->pSolFans = ABC_ALLOC( int, 2 * p->nNodes ); + for ( i = p->nVars; i < p->nObjs; i++ ) + for ( k = 1; k >= 0; k-- ) + p->pPars->pSolFans[Pos++] = Exa_ManFindFanin( p, i, k ); +} /**Function************************************************************* @@ -716,6 +788,39 @@ static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits ) } return bmcg_sat_solver_addclause( p->pSat, pLits, nLits ); } +static int Exa_ManAddPermConstr( Exa_Man_t * p ) +{ + int i, k, iVar, Lit; + char Name0[16], Name1[16]; + if ( p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL ) + return 1; + Exa_ManPrintFixedPerm( p ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + for ( k = 0; k < 2; k++ ) + { + iVar = Exa_ManPermFanin( p, i, k ); + if ( iVar == -1 ) + continue; + if ( iVar < 0 || iVar >= p->nVars || p->VarMarks[i][k][iVar] == 0 ) + { + if ( iVar >= p->nVars && iVar < i && p->VarMarks[i][k][iVar] ) + { + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !Exa_ManAddClause( p, &Lit, 1 ) ) + return 0; + continue; + } + printf( "Cannot force node %s fanin %d to object %s because this connection is not available.\n", Exa_ManObjName(p, i, Name0), k, Exa_ManObjName(p, iVar, Name1) ); + return 0; + } + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !Exa_ManAddClause( p, &Lit, 1 ) ) + return 0; + } + } + return 1; +} int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded ) { int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m; @@ -794,6 +899,8 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) assert( n == p->nVars + p->nNodes ); Vec_IntFreeP( &vRes ); } + if ( !Exa_ManAddPermConstr(p) ) + return 0; // input constraints for ( i = p->nVars; i < p->nObjs; i++ ) { @@ -946,9 +1053,10 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) p->iVar += 3*p->nNodes; return 1; } -void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) +int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; + int fFound = 0; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); @@ -956,8 +1064,13 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); - assert( status ); - printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); + if ( !status ) + { + Exa_ManFree( p ); + return 0; + } + if ( !pPars->fSilent ) + printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); for ( i = 0; iMint != -1; i++ ) { abctime clk = Abc_Clock(); @@ -978,23 +1091,33 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) } if ( status == GLUCOSE_UNSAT ) { - printf( "The problem has no solution.\n" ); + if ( !pPars->fSilent ) + printf( "The problem has no solution.\n" ); break; } if ( status == GLUCOSE_UNDEC ) { - printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); + if ( !pPars->fSilent ) + printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); break; } iMint = Exa_ManEval( p ); } if ( iMint == -1 ) { - Exa_ManPrintSolution( p, fCompl ); - Exa_ManDumpBlif( p, fCompl ); + Exa_ManSaveSolution( p ); + if ( !pPars->fSilent ) + { + Exa_ManPrintSolution( p, fCompl ); + Exa_ManPrintPerm( p ); + Exa_ManDumpBlif( p, fCompl ); + } + fFound = 1; } Exa_ManFree( p ); - Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( !pPars->fSilent ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + return fFound; } diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 761795d96..87f3a6920 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -577,7 +577,8 @@ static int Exa_ManMarkup( Exa_Man_t * p ) } } } - printf( "The number of parameter variables = %d.\n", p->iVar ); + if ( !p->pPars->fSilent ) + printf( "The number of parameter variables = %d.\n", p->iVar ); return p->iVar; // printout for ( i = p->nVars; i < p->nObjs; i++ ) @@ -640,6 +641,18 @@ static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k ) assert( Count == 1 ); return iVar; } +static inline char * Exa_ManObjName( Exa_Man_t * p, int iObj, char * pBuffer ) +{ + if ( iObj < 0 ) + sprintf( pBuffer, "*" ); + else if ( iObj < p->nVars ) + sprintf( pBuffer, "%c", 'a' + iObj ); + else if ( iObj - p->nVars < 26 ) + sprintf( pBuffer, "%c", 'A' + iObj - p->nVars ); + else + sprintf( pBuffer, "N%d", iObj - p->nVars ); + return pBuffer; +} static inline int Exa_ManEval( Exa_Man_t * p ) { static int Flag = 0; @@ -681,6 +694,7 @@ static inline int Exa_ManEval( Exa_Man_t * p ) static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) { int i, k, iVar; + char Name[16]; printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes ); // for ( i = p->nVars + 2; i < p->nObjs; i++ ) for ( i = p->nObjs - 1; i >= p->nVars; i-- ) @@ -690,20 +704,113 @@ static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) int Val2 = sat_solver_var_value(p->pSat, iVarStart+1); int Val3 = sat_solver_var_value(p->pSat, iVarStart+2); if ( i == p->nObjs - 1 && fCompl ) - printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 ); + printf( "%s = 4\'b%d%d%d1(", Exa_ManObjName(p, i, Name), !Val3, !Val2, !Val1 ); else - printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 ); + printf( "%s = 4\'b%d%d%d0(", Exa_ManObjName(p, i, Name), Val3, Val2, Val1 ); for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - if ( iVar >= 0 && iVar < p->nVars ) - printf( " %c", 'a'+iVar ); - else - printf( " %02d", iVar ); + printf( " %s", Exa_ManObjName(p, iVar, Name) ); } printf( " )\n" ); } } +static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k ) +{ + char * pPermStr = p->pPars->pPermStr; + int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1); + int nSeen = 0, s; + if ( p->pPars->pPermFans ) + return p->pPars->pPermFans[iTarget]; + assert( pPermStr != NULL ); + for ( s = 0; pPermStr[s]; s++ ) + { + if ( pPermStr[s] == '_' ) + continue; + if ( nSeen++ == iTarget ) + return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a'; + } + assert( 0 ); + return -1; +} +static void Exa_ManPrintPermFanin( Exa_Man_t * p, int iFanin ) +{ + char Name[16]; + printf( "%s ", Exa_ManObjName(p, iFanin, Name) ); +} +static void Exa_ManPrintFixedPerm( Exa_Man_t * p ) +{ + int i, k; + char Name[16]; + if ( (p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL) || p->pPars->fSilent ) + return; + printf( "Using fixed input assignment provided by the user %s:\n", p->pPars->pPermStr ? p->pPars->pPermStr : "" ); + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) + { + printf( "%s : ", Exa_ManObjName(p, i, Name) ); + for ( k = 1; k >= 0; k-- ) + Exa_ManPrintPermFanin( p, Exa_ManPermFanin(p, i, k) ); + printf( "\n" ); + } +} +static void Exa_ManPrintPerm( Exa_Man_t * p ) +{ + int i, k, iVar; + printf( "The variable permutation is \"" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + if ( i > p->nVars ) + printf( "_" ); + for ( k = 1; k >= 0; k-- ) + { + iVar = Exa_ManFindFanin( p, i, k ); + printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' ); + } + } + printf( "\".\n" ); +} +static void Exa_ManSaveSolution( Exa_Man_t * p ) +{ + int i, k, Pos = 0; + ABC_FREE( p->pPars->pSolFans ); + p->pPars->pSolFans = ABC_ALLOC( int, 2 * p->nNodes ); + for ( i = p->nVars; i < p->nObjs; i++ ) + for ( k = 1; k >= 0; k-- ) + p->pPars->pSolFans[Pos++] = Exa_ManFindFanin( p, i, k ); +} +static int Exa_ManAddPermConstr( Exa_Man_t * p ) +{ + int i, k, iVar, Lit; + char Name0[16], Name1[16]; + if ( p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL ) + return 1; + Exa_ManPrintFixedPerm( p ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + for ( k = 0; k < 2; k++ ) + { + iVar = Exa_ManPermFanin( p, i, k ); + if ( iVar == -1 ) + continue; + if ( iVar < 0 || iVar >= p->nVars || p->VarMarks[i][k][iVar] == 0 ) + { + if ( iVar >= p->nVars && iVar < i && p->VarMarks[i][k][iVar] ) + { + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ) ) + return 0; + continue; + } + printf( "Cannot force node %s fanin %d to object %s because this connection is not available.\n", Exa_ManObjName(p, i, Name0), k, Exa_ManObjName(p, iVar, Name1) ); + return 0; + } + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ) ) + return 0; + } + } + return 1; +} /**Function************************************************************* @@ -720,6 +827,8 @@ static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) { int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m; + if ( !Exa_ManAddPermConstr(p) ) + return 0; // input constraints for ( i = p->nVars; i < p->nObjs; i++ ) { @@ -849,9 +958,10 @@ static int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) p->iVar += 3*p->nNodes; return 1; } -void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) +int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; + int fFound = 0; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); @@ -859,8 +969,13 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); - assert( status ); - printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); + if ( !status ) + { + Exa_ManFree( p ); + return 0; + } + if ( !pPars->fSilent ) + printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); for ( i = 0; iMint != -1; i++ ) { abctime clk = Abc_Clock(); @@ -878,15 +993,26 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) } if ( status == l_False ) { - printf( "The problem has no solution.\n" ); + if ( !pPars->fSilent ) + printf( "The problem has no solution.\n" ); break; } iMint = Exa_ManEval( p ); } if ( iMint == -1 ) - Exa_ManPrintSolution( p, fCompl ); + { + Exa_ManSaveSolution( p ); + if ( !pPars->fSilent ) + { + Exa_ManPrintSolution( p, fCompl ); + Exa_ManPrintPerm( p ); + } + fFound = 1; + } Exa_ManFree( p ); - Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( !pPars->fSilent ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + return fFound; } From ffb0ff63fc5adb13c4d7aeb36e12c0f3af0a4403 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 May 2026 07:23:18 -0700 Subject: [PATCH 05/13] Updating interface of %yosys to take multiple Verilog files. --- src/base/wln/wlnCom.c | 111 ++++++++++++++++++++++++-------------- src/base/wln/wlnRtl.c | 123 ++++++++++++++++++++++++++++++------------ 2 files changed, 160 insertions(+), 74 deletions(-) diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index 2436932cd..e471bc877 100644 --- a/src/base/wln/wlnCom.c +++ b/src/base/wln/wlnCom.c @@ -92,13 +92,16 @@ void Wln_End( Abc_Frame_t * pAbc ) ******************************************************************************/ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ); - extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); - extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ); + extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ); + extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); + extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ); FILE * pFile; char * pFileName = NULL; char * pFileName2= NULL; + char ** ppFileNames = NULL; + int nFileNames = 0; + int fFileNamesAlloc = 0; char * pTopModule= NULL; char * pDefines = NULL; char * pLibrary = NULL; @@ -194,48 +197,64 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( argc != globalUtilOptind + 1 ) + nFileNames = argc - globalUtilOptind; + if ( nFileNames < 1 ) { - printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" ); + printf( "Abc_CommandReadWlc(): Input file name(s) should be given on the command line.\n" ); return 0; } - // get the file name - pFileName = argv[globalUtilOptind]; - if ( (pFile = fopen( pFileName, "r" )) == NULL ) - { - Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName ); - if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) ) - Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); - Abc_Print( 1, "\n" ); - return 0; - } - fclose( pFile ); + ppFileNames = pFileName2 ? ABC_ALLOC( char *, nFileNames + 1 ) : argv + globalUtilOptind; + fFileNamesAlloc = pFileName2 != NULL; if ( pFileName2 ) { - if ( (pFile = fopen( pFileName2, "r" )) == NULL ) + int i; + for ( i = 0; i < nFileNames; i++ ) + ppFileNames[i] = argv[globalUtilOptind + i]; + ppFileNames[nFileNames++] = pFileName2; + } + pFileName = ppFileNames[0]; + for ( c = 0; c < nFileNames; c++ ) + { + if ( (pFile = fopen( ppFileNames[c], "r" )) == NULL ) { - Abc_Print( 1, "Cannot open input file \"%s\".\n", pFileName2 ); + Abc_Print( 1, "Cannot open input file \"%s\". ", ppFileNames[c] ); + if ( (pFileName = Extra_FileGetSimilarName( ppFileNames[c], ".v", ".sv", NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); + Abc_Print( 1, "\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } fclose( pFile ); } - - // perform reading - if ( pLibrary ) + pFileName = ppFileNames[0]; + if ( nFileNames > 1 ) { - if ( pFileName2 ) + int i, fAllVerilog = 1; + for ( i = 0; i < nFileNames; i++ ) + fAllVerilog &= Extra_FileIsType( ppFileNames[i], ".v", ".sv", NULL ); + if ( !fAllVerilog ) { - Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); + Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } + } + + // perform reading + if ( pLibrary ) + { Abc_Ntk_t * pNtk = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose ); + pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose ); + pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose ); else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); @@ -244,55 +263,67 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pNew = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) { - if ( pFileName2 ) + if ( nFileNames > 1 ) { - Abc_Print( 1, "Command line switch \"-F\" is only supported when the main input is Verilog/SystemVerilog.\n" ); + Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } - pNew = Wln_BlastSystemVerilog( pFileName, NULL, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); } else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } Abc_FrameUpdateGia( pAbc, pNew ); } else { - if ( pFileName2 ) - { - Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); - return 0; - } Rtl_Lib_t * pLib = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); + pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); + pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); + { + if ( nFileNames > 1 ) + { + Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); + return 0; + } + pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose ); + } else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } Wln_AbcUpdateRtl( pAbc, pLib ); } + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; usage: - Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-F ] [-bdisumlcvh] \n" ); + Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-F ] [-bdisumlcvh] [file_name...]\n" ); Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" ); Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" ); Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" ); Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" ); Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" ); - Abc_Print( -2, "\t-F : specify a second Verilog/SystemVerilog file for the default bit-blasting flow (default \"not used\")\n" ); + Abc_Print( -2, "\t-F : specify an additional Verilog/SystemVerilog file (default \"not used\")\n" ); Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" ); Abc_Print( -2, "\t-d : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" ); diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index ffe8e457d..f9ed19924 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -122,6 +122,30 @@ char * Wln_GetYosysName() #endif return pYosysName; } +static char * Wln_FileNamesJoin( char ** ppFileNames, int nFileNames ) +{ + char * pFileNames; + int i, nChars = 1; + for ( i = 0; i < nFileNames; i++ ) + nChars += strlen( ppFileNames[i] ) + 1; + pFileNames = ABC_ALLOC( char, nChars ); + pFileNames[0] = 0; + for ( i = 0; i < nFileNames; i++ ) + { + if ( i ) + strcat( pFileNames, " " ); + strcat( pFileNames, ppFileNames[i] ); + } + return pFileNames; +} +static int Wln_FileNamesHasSv( char ** ppFileNames, int nFileNames ) +{ + int i; + for ( i = 0; i < nFileNames; i++ ) + if ( strstr( ppFileNames[i], ".sv" ) != NULL ) + return 1; + return 0; +} int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) { #if defined(__wasm) @@ -142,29 +166,39 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) return 1; #endif } -Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ) +Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ) { Rtl_Lib_t * pNtk = NULL; - char Command[1000]; + char * pFileNames, * pCommand; char * pFileTemp = "_temp_.rtlil"; - int fSVlog = strstr(pFileName, ".sv") != NULL; - if ( strstr(pFileName, ".rtl") ) - return Rtl_LibReadFile( pFileName, pFileName ); - sprintf( Command, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"", + int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); + int nCommand; + if ( nFileNames == 1 && strstr(ppFileNames[0], ".rtl") ) + return Rtl_LibReadFile( ppFileNames[0], ppFileNames[0] ); + pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); + nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 200; + pCommand = ABC_ALLOC( char, nCommand ); + sprintf( pCommand, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"", Wln_GetYosysName(), pDefines ? "-D" : "", pDefines ? pDefines : "", fSVlog ? "-sv " : "", - pFileName, + pFileNames, pTopModule ? "-top " : "", pTopModule ? pTopModule : "", fCollapse ? "flatten; ": "", pFileTemp ); if ( fVerbose ) - printf( "%s\n", Command ); - if ( !Wln_ConvertToRtl(Command, pFileTemp) ) + printf( "%s\n", pCommand ); + if ( !Wln_ConvertToRtl(pCommand, pFileTemp) ) + { + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); return NULL; - pNtk = Rtl_LibReadFile( pFileTemp, pFileName ); + } + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + pNtk = Rtl_LibReadFile( pFileTemp, ppFileNames[0] ); if ( pNtk == NULL ) { printf( "Dumped the design into file \"%s\".\n", pFileTemp ); @@ -174,33 +208,41 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p unlink( pFileTemp ); return pNtk; } -Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) +Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) { Gia_Man_t * pGia = NULL; - char Command[1000]; + char * pFileNames, * pCommand; char * pFileTemp = "_temp_.aig"; - int fRtlil = strstr(pFileName, ".rtl") != NULL; - int fSVlog = strstr(pFileName, ".sv") != NULL || (pFileName2 && strstr(pFileName2, ".sv") != NULL); - sprintf( Command, "%s -qp \"%s %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", + int fRtlil = nFileNames == 1 && strstr(ppFileNames[0], ".rtl") != NULL; + int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); + int nCommand; + pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); + nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 500; + pCommand = ABC_ALLOC( char, nCommand ); + sprintf( pCommand, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", Wln_GetYosysName(), fRtlil ? "read_rtlil" : "read_verilog", pDefines ? "-D" : "", pDefines ? pDefines : "", fSVlog ? "-sv " : "", - pFileName, - pFileName2 ? " " : "", - pFileName2 ? pFileName2 : "", + pFileNames, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "", fSetUndef ? "setundef -init -zero; " : "", - pFileName2 ? "delete t:\\$scopeinfo; " : "", + nFileNames > 1 ? "delete t:\\$scopeinfo; " : "", pFileTemp ); if ( fVerbose ) - printf( "%s\n", Command ); - if ( !Wln_ConvertToRtl(Command, pFileTemp) ) + printf( "%s\n", pCommand ); + if ( !Wln_ConvertToRtl(pCommand, pFileTemp) ) + { + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); return NULL; - if ( pFileName2 ) + } + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + if ( nFileNames > 1 ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = NULL; @@ -229,7 +271,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * } ABC_FREE( pGia->pName ); pGia->pName = pTopModule ? Abc_UtilStrsav(pTopModule) : - Extra_FileNameGeneric( Extra_FileNameWithoutPath(pFileName) ); + Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) ); unlink( pFileTemp ); // complement the outputs if ( fInvert ) @@ -240,35 +282,48 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * } return pGia; } -Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ) +Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ) { Abc_Ntk_t * pNtk = NULL; - char Command[1000]; + char * pFileNames, * pCommand; char * pFileTemp = "_temp_.blif"; - int fSVlog = strstr(pFileName, ".sv") != NULL; - sprintf( Command, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"", + int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); + int nCommand; + pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); + nCommand = strlen(Wln_GetYosysName()) + strlen(pLibrary) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 300; + pCommand = ABC_ALLOC( char, nCommand ); + sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"", Wln_GetYosysName(), pLibrary, fSVlog ? "-sv " : "-vlog95", pDefines ? "-D" : "", pDefines ? pDefines : "", - pFileName, + pFileNames, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", pTopModule ? "-top " : "", pTopModule ? pTopModule : "", pFileTemp ); if ( fVerbose ) - printf( "%s\n", Command ); - if ( !Wln_ConvertToRtl(Command, pFileTemp) ) - return NULL; - sprintf( Command, "read_lib %s", pLibrary ); - if ( Cmd_CommandExecute( Abc_FrameReadGlobalFrame(), Command ) ) + printf( "%s\n", pCommand ); + if ( !Wln_ConvertToRtl(pCommand, pFileTemp) ) { - fprintf( stdout, "Cannot execute ABC command \"%s\".\n", Command ); + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + return NULL; + } + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + pCommand = ABC_ALLOC( char, strlen(pLibrary) + 20 ); + sprintf( pCommand, "read_lib %s", pLibrary ); + if ( Cmd_CommandExecute( Abc_FrameReadGlobalFrame(), pCommand ) ) + { + fprintf( stdout, "Cannot execute ABC command \"%s\".\n", pCommand ); + ABC_FREE( pCommand ); unlink( pFileTemp ); return NULL; } + ABC_FREE( pCommand ); pNtk = Io_Read( pFileTemp, IO_FILE_BLIF, 1, 0 ); if ( pNtk == NULL ) { From f4d870e109938fd1a283ecceea950bd9cd616f67 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 18 May 2026 07:31:39 -0700 Subject: [PATCH 06/13] Updating interface of "twoexaxct". --- src/base/abci/abc.c | 53 +++++++++++++++++++++++++++++++++++++------ src/sat/bmc/bmcMaj.c | 37 ++++++++++++++++++++++++++---- src/sat/bmc/bmcMaj2.c | 37 ++++++++++++++++++++++++++---- 3 files changed, 110 insertions(+), 17 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c84663fd9..543eb5f5c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10720,6 +10720,41 @@ static char * Abc_TwoExactPermEncodeFull( int * pFans, int nVars, int nNodes ) pPerm[Pos] = 0; return pPerm; } +static int Abc_TwoExactPermParseObj( char ** ppToken, int nVars, int nNodes, int * pObj ) +{ + char * pToken = *ppToken; + if ( *pToken == '*' ) + { + *pObj = -1; + *ppToken = pToken + 1; + return 1; + } + if ( *pToken >= 'a' && *pToken < 'a' + nVars ) + { + *pObj = *pToken - 'a'; + *ppToken = pToken + 1; + return 1; + } + if ( *pToken >= 'A' && *pToken <= 'Z' ) + { + *pObj = nVars + *pToken - 'A'; + *ppToken = pToken + 1; + return *pObj < nVars + nNodes; + } + if ( *pToken == 'N' ) + { + char * pNext = pToken + 1; + int Num = 0; + if ( *pNext < '0' || *pNext > '9' ) + return 0; + while ( *pNext >= '0' && *pNext <= '9' ) + Num = 10 * Num + *pNext++ - '0'; + *pObj = nVars + Num; + *ppToken = pNext; + return *pObj < nVars + nNodes; + } + return 0; +} static int Abc_TwoExactPermAddDcs( int * pFans, int nVars, int nNodes, int nDcs, int nSkip, int fAll ) { int i, k, nLetters = 0; @@ -11164,15 +11199,19 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pPars->pPermStr ) { - int i, nEntries = 0; - for ( i = 0; pPars->pPermStr[i]; i++ ) + char * pToken = pPars->pPermStr; + int nEntries = 0; + while ( *pToken ) { - char Sym = pPars->pPermStr[i]; - if ( Sym == '_' ) - continue; - if ( Sym != '*' && (Sym < 'a' || Sym >= 'a' + pPars->nVars) ) + int iObj = -1; + if ( *pToken == '_' ) { - Abc_Print( -1, "Permutation symbol \"%c\" is not one of '*', '_' or input variables 'a' through '%c'.\n", Sym, 'a' + pPars->nVars - 1 ); + pToken++; + continue; + } + if ( !Abc_TwoExactPermParseObj(&pToken, pPars->nVars, pPars->nNodes, &iObj) ) + { + Abc_Print( -1, "Permutation should use '*', '_', input variables 'a' through '%c', or internal nodes 'A' through '%c'.\n", 'a' + pPars->nVars - 1, 'A' + Abc_MinInt(pPars->nNodes, 26) - 1 ); return 1; } nEntries++; diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index eadcd08ad..b5831e7ff 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -704,16 +704,42 @@ static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k ) { char * pPermStr = p->pPars->pPermStr; int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1); - int nSeen = 0, s; + int nSeen = 0; + char * pToken; if ( p->pPars->pPermFans ) return p->pPars->pPermFans[iTarget]; assert( pPermStr != NULL ); - for ( s = 0; pPermStr[s]; s++ ) + for ( pToken = pPermStr; *pToken; ) { - if ( pPermStr[s] == '_' ) + int iObj = -2; + if ( *pToken == '_' ) + { + pToken++; continue; + } + if ( *pToken == '*' ) + { + iObj = -1; + pToken++; + } + else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars ) + iObj = *pToken++ - 'a'; + else if ( *pToken >= 'A' && *pToken <= 'Z' ) + iObj = p->nVars + (*pToken++ - 'A'); + else if ( *pToken == 'N' ) + { + char * pNext = pToken + 1; + int Num = 0; + assert( *pNext >= '0' && *pNext <= '9' ); + while ( *pNext >= '0' && *pNext <= '9' ) + Num = 10 * Num + *pNext++ - '0'; + iObj = p->nVars + Num; + pToken = pNext; + } + else + assert( 0 ); if ( nSeen++ == iTarget ) - return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a'; + return iObj; } assert( 0 ); return -1; @@ -741,6 +767,7 @@ static void Exa_ManPrintFixedPerm( Exa_Man_t * p ) static void Exa_ManPrintPerm( Exa_Man_t * p ) { int i, k, iVar; + char Name[16]; printf( "The variable permutation is \"" ); for ( i = p->nVars; i < p->nObjs; i++ ) { @@ -749,7 +776,7 @@ static void Exa_ManPrintPerm( Exa_Man_t * p ) for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' ); + printf( "%s", Exa_ManObjName(p, iVar, Name) ); } } printf( "\".\n" ); diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 87f3a6920..23ccb7217 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -719,16 +719,42 @@ static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k ) { char * pPermStr = p->pPars->pPermStr; int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1); - int nSeen = 0, s; + int nSeen = 0; + char * pToken; if ( p->pPars->pPermFans ) return p->pPars->pPermFans[iTarget]; assert( pPermStr != NULL ); - for ( s = 0; pPermStr[s]; s++ ) + for ( pToken = pPermStr; *pToken; ) { - if ( pPermStr[s] == '_' ) + int iObj = -2; + if ( *pToken == '_' ) + { + pToken++; continue; + } + if ( *pToken == '*' ) + { + iObj = -1; + pToken++; + } + else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars ) + iObj = *pToken++ - 'a'; + else if ( *pToken >= 'A' && *pToken <= 'Z' ) + iObj = p->nVars + (*pToken++ - 'A'); + else if ( *pToken == 'N' ) + { + char * pNext = pToken + 1; + int Num = 0; + assert( *pNext >= '0' && *pNext <= '9' ); + while ( *pNext >= '0' && *pNext <= '9' ) + Num = 10 * Num + *pNext++ - '0'; + iObj = p->nVars + Num; + pToken = pNext; + } + else + assert( 0 ); if ( nSeen++ == iTarget ) - return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a'; + return iObj; } assert( 0 ); return -1; @@ -756,6 +782,7 @@ static void Exa_ManPrintFixedPerm( Exa_Man_t * p ) static void Exa_ManPrintPerm( Exa_Man_t * p ) { int i, k, iVar; + char Name[16]; printf( "The variable permutation is \"" ); for ( i = p->nVars; i < p->nObjs; i++ ) { @@ -764,7 +791,7 @@ static void Exa_ManPrintPerm( Exa_Man_t * p ) for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' ); + printf( "%s", Exa_ManObjName(p, iVar, Name) ); } } printf( "\".\n" ); From 70c42b729298584cfb18577f205f644dfb254f9e Mon Sep 17 00:00:00 2001 From: Franz Reichl Date: Thu, 21 May 2026 11:58:13 +0200 Subject: [PATCH 07/13] Add option for lut optimisation --- src/base/abci/abc.c | 2 +- src/opt/eslim/eSLIM.cpp | 10 ++++------ src/opt/eslim/eslimCirMan.cpp | 1 + 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 543eb5f5c..20b9a6cf1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -61036,7 +61036,7 @@ int Abc_CommandAbc9elSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) { seteSLIMParams(¶ms); Extra_UtilGetoptReset(); params.subcircuit_max_size = 4; - while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZfhist" ) ) != EOF ) { + while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZcfhist" ) ) != EOF ) { switch ( c ) { case 'C': if ( globalUtilOptind >= argc ) diff --git a/src/opt/eslim/eSLIM.cpp b/src/opt/eslim/eSLIM.cpp index 670551568..764c822e1 100644 --- a/src/opt/eslim/eSLIM.cpp +++ b/src/opt/eslim/eSLIM.cpp @@ -603,6 +603,10 @@ Circuitrepresentation* runeSLIM(Circuitrepresentation * cir, const eSLIM_ParamSt Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) { + if (Gia_ManHasDangling(pGia)) { + std::cout << "Warning: Circuit must not contain dangling nodes.\n"; + return pGia; + } return runeSLIM(pGia, params); } @@ -610,12 +614,6 @@ Abc_Ntk_t* applyelSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) { return runeSLIM(ntk, params); } -Abc_Ntk_t* applyetSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) { - return runeSLIM(ntk, params); -} - - - diff --git a/src/opt/eslim/eslimCirMan.cpp b/src/opt/eslim/eslimCirMan.cpp index 38e1635cd..5f9c5007d 100644 --- a/src/opt/eslim/eslimCirMan.cpp +++ b/src/opt/eslim/eslimCirMan.cpp @@ -79,6 +79,7 @@ namespace eSLIM { } eSLIMCirMan::eSLIMCirMan(Gia_Man_t * pGia) : eSLIMCirMan(Gia_ManObjNum(pGia)) { + assert (!Gia_ManHasDangling(pGia)); Gia_ManConst0(pGia)->Value = 0; Gia_Obj_t * pObj; int i; From cd6e9b582ba757017c2c54613d342cb7a8a4b04a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 21 May 2026 23:41:12 -0700 Subject: [PATCH 08/13] Modify default intermediate AIGER file name. --- src/base/abci/abc.c | 23 ++++++++++++++++++----- src/base/wln/wlnRtl.c | 12 +++++++++++- 2 files changed, 29 insertions(+), 6 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 543eb5f5c..8716bf04e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43284,6 +43284,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam Gia_Man_t * pGia; char * pTemp; char * pOrigFileName = NULL; + char * pFileTemp = NULL; int fVerilog, fSystemVerilog; *pAbc_ReadAigerOrVerilogFileStatus = 0; @@ -43312,17 +43313,24 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = NULL; char pCommand[2000]; + char * pFileBase; int RetValue; int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL ); // Save the original filename before changing it pOrigFileName = pFileName; + pFileBase = pTopModule ? Abc_UtilStrsav(pTopModule) : + Extra_FileNameGeneric( Extra_FileNameWithoutPath(pFileName) ); + pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 ); + sprintf( pFileTemp, "%s.aig", pFileBase ); + ABC_FREE( pFileBase ); snprintf( pCommand, sizeof(pCommand), - "yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols _temp_.aig\"", + "yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", pDefines ? "-D" : "", pDefines ? pDefines : "", (fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName, pFileName2 ? " " : "", pFileName2 ? pFileName2 : "", pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", - pFileName2 ? "delete t:\\$scopeinfo; " : "" ); + pFileName2 ? "delete t:\\$scopeinfo; " : "", + pFileTemp ); #if defined(__wasm) RetValue = 1; #else @@ -43331,14 +43339,16 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam if ( RetValue != 0 ) { Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand ); + ABC_FREE( pFileTemp ); return NULL; } if ( pFileName2 ) { - Abc_Ntk_t * pNtk = Io_Read( "_temp_.aig", IO_FILE_AIGER, 1, 0 ); + Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); if ( pNtk == NULL ) { - Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", "_temp_.aig" ); + Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileTemp ); + ABC_FREE( pFileTemp ); return NULL; } pAig = Abc_NtkToDar( pNtk, 0, 1 ); @@ -43346,6 +43356,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam if ( pAig == NULL ) { Abc_Print( -1, "Converting the AIGER network into an internal AIG has failed.\n" ); + ABC_FREE( pFileTemp ); return NULL; } pGia = Gia_ManFromAig( pAig ); @@ -43353,7 +43364,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam } else { - pFileName = "_temp_.aig"; + pFileName = pFileTemp; pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); } } @@ -43362,6 +43373,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName ); + ABC_FREE( pFileTemp ); return NULL; } @@ -43372,6 +43384,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam pGia->pSpec = Abc_UtilStrsav( pOrigFileName ); } + ABC_FREE( pFileTemp ); return pGia; } diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index f9ed19924..fe103557a 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -212,10 +212,15 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * { Gia_Man_t * pGia = NULL; char * pFileNames, * pCommand; - char * pFileTemp = "_temp_.aig"; + char * pFileTemp, * pFileBase; int fRtlil = nFileNames == 1 && strstr(ppFileNames[0], ".rtl") != NULL; int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); int nCommand; + pFileBase = pTopModule ? Abc_UtilStrsav(pTopModule) : + Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) ); + pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 ); + sprintf( pFileTemp, "%s.aig", pFileBase ); + ABC_FREE( pFileBase ); pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 500; pCommand = ABC_ALLOC( char, nCommand ); @@ -238,6 +243,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * { ABC_FREE( pCommand ); ABC_FREE( pFileNames ); + ABC_FREE( pFileTemp ); return NULL; } ABC_FREE( pCommand ); @@ -250,6 +256,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * if ( pNtk == NULL ) { printf( "Reading AIGER from file \"%s\" has failed.\n", pFileTemp ); + ABC_FREE( pFileTemp ); return NULL; } pAig = Abc_NtkToDar( pNtk, 0, 1 ); @@ -257,6 +264,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * if ( pAig == NULL ) { printf( "Converting the AIGER network into an internal AIG has failed.\n" ); + ABC_FREE( pFileTemp ); return NULL; } pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig); @@ -267,12 +275,14 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * if ( pGia == NULL ) { printf( "Converting to AIG has failed.\n" ); + ABC_FREE( pFileTemp ); return NULL; } ABC_FREE( pGia->pName ); pGia->pName = pTopModule ? Abc_UtilStrsav(pTopModule) : Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) ); unlink( pFileTemp ); + ABC_FREE( pFileTemp ); // complement the outputs if ( fInvert ) { From 21b2d8959a7f0cf61cc1975eabb0489d901a47f8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 4 Jun 2026 21:05:04 +0700 Subject: [PATCH 09/13] Add output name permutation in &cec. --- src/base/abci/abc.c | 113 ++++++++++++++++++++++++++++++++++++++++++ src/base/wln/wlnRtl.c | 20 ++++++++ 2 files changed, 133 insertions(+) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 44ceacc88..a8d056979 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43267,6 +43267,105 @@ static Gia_Man_t * Abc_GiaReorderInputsByName( Gia_Man_t * pFirst, Gia_Man_t * p return pNew; } +static Gia_Man_t * Abc_GiaDupPermOutputs( Gia_Man_t * p, Vec_Int_t * vPoPerm ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + assert( Vec_IntSize(vPoPerm) == Gia_ManPoNum(p) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( Gia_ObjIsBuf(pObj) ) + pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + else + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm, i))) ); + Gia_ManForEachRi( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +static Gia_Man_t * Abc_GiaReorderOutputsByName( Gia_Man_t * pFirst, Gia_Man_t * pSecond ) +{ + Vec_Int_t * vPoPerm; + Gia_Man_t * pNew; + char * pName1, * pName2; + int * pUsed; + int i, k, nPos, fDiff = 0; + if ( pFirst == NULL || pSecond == NULL || pFirst->vNamesOut == NULL || pSecond->vNamesOut == NULL ) + return NULL; + nPos = Gia_ManPoNum( pFirst ); + if ( nPos != Gia_ManPoNum(pSecond) ) + return NULL; + if ( Vec_PtrSize(pFirst->vNamesOut) < nPos || Vec_PtrSize(pSecond->vNamesOut) < nPos ) + return NULL; + vPoPerm = Vec_IntAlloc( nPos ); + pUsed = ABC_CALLOC( int, nPos ); + for ( i = 0; i < nPos; i++ ) + { + pName1 = (char *)Vec_PtrEntry( pFirst->vNamesOut, i ); + if ( pName1 == NULL ) + break; + for ( k = 0; k < nPos; k++ ) + { + pName2 = (char *)Vec_PtrEntry( pSecond->vNamesOut, k ); + if ( pName2 && !pUsed[k] && !strcmp(pName1, pName2) ) + break; + } + if ( k == nPos ) + break; + pUsed[k] = 1; + Vec_IntPush( vPoPerm, k ); + fDiff |= (k != i); + } + ABC_FREE( pUsed ); + if ( i < nPos || !fDiff ) + { + Vec_IntFree( vPoPerm ); + return NULL; + } + pNew = Abc_GiaDupPermOutputs( pSecond, vPoPerm ); + Vec_IntFree( vPoPerm ); + pNew->vNamesIn = Abc_GiaDupNameVec( pSecond->vNamesIn ); + pNew->vNamesOut = Vec_PtrAlloc( Vec_PtrSize(pSecond->vNamesOut) ); + for ( i = 0; i < nPos; i++ ) + { + pName1 = (char *)Vec_PtrEntry( pFirst->vNamesOut, i ); + Vec_PtrPush( pNew->vNamesOut, pName1 ? Abc_UtilStrsav(pName1) : NULL ); + } + for ( i = nPos; i < Vec_PtrSize(pSecond->vNamesOut); i++ ) + { + pName2 = (char *)Vec_PtrEntry( pSecond->vNamesOut, i ); + Vec_PtrPush( pNew->vNamesOut, pName2 ? Abc_UtilStrsav(pName2) : NULL ); + } + return pNew; +} + +static void Abc_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames ) +{ + if ( pGia == NULL || pGiaNames == NULL ) + return; + if ( pGia->vNamesIn == NULL && pGiaNames->vNamesIn != NULL && Gia_ManCiNum(pGia) == Vec_PtrSize(pGiaNames->vNamesIn) ) + { + pGia->vNamesIn = pGiaNames->vNamesIn; + pGiaNames->vNamesIn = NULL; + } + if ( pGia->vNamesOut == NULL && pGiaNames->vNamesOut != NULL && Gia_ManCoNum(pGia) == Vec_PtrSize(pGiaNames->vNamesOut) ) + { + pGia->vNamesOut = pGiaNames->vNamesOut; + pGiaNames->vNamesOut = NULL; + } +} + /**Function************************************************************* Synopsis [] @@ -43344,6 +43443,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam } if ( pFileName2 ) { + Gia_Man_t * pGiaNames = NULL; Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); if ( pNtk == NULL ) { @@ -43361,6 +43461,10 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam } pGia = Gia_ManFromAig( pAig ); Aig_ManStop( pAig ); + pGiaNames = Gia_AigerRead( pFileTemp, 0, 1, 0 ); + Abc_GiaTransferNamesIfMatch( pGia, pGiaNames ); + if ( pGiaNames ) + Gia_ManStop( pGiaNames ); } else { @@ -43644,6 +43748,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManStop( pGias[1] ); pGias[1] = pTemp; } + pTemp = Abc_GiaReorderOutputsByName( pGias[0], pGias[1] ); + if ( pTemp ) + { + if ( pPars->fVerbose ) + Abc_Print( 1, "Reordered primary outputs of the second network using output names.\n" ); + if ( pGias[1] != pAbc->pGia && pGias[1] != pAbc->pGiaSaved ) + Gia_ManStop( pGias[1] ); + pGias[1] = pTemp; + } } pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL; pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL; diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index fe103557a..6c92cffbc 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -146,6 +146,21 @@ static int Wln_FileNamesHasSv( char ** ppFileNames, int nFileNames ) return 1; return 0; } +static void Wln_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames ) +{ + if ( pGia == NULL || pGiaNames == NULL ) + return; + if ( pGia->vNamesIn == NULL && pGiaNames->vNamesIn != NULL && Gia_ManCiNum(pGia) == Vec_PtrSize(pGiaNames->vNamesIn) ) + { + pGia->vNamesIn = pGiaNames->vNamesIn; + pGiaNames->vNamesIn = NULL; + } + if ( pGia->vNamesOut == NULL && pGiaNames->vNamesOut != NULL && Gia_ManCoNum(pGia) == Vec_PtrSize(pGiaNames->vNamesOut) ) + { + pGia->vNamesOut = pGiaNames->vNamesOut; + pGiaNames->vNamesOut = NULL; + } +} int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) { #if defined(__wasm) @@ -252,6 +267,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = NULL; + Gia_Man_t * pGiaNames = NULL; Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); if ( pNtk == NULL ) { @@ -269,6 +285,10 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * } pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig); Aig_ManStop( pAig ); + pGiaNames = Gia_AigerRead( pFileTemp, 0, 1, 0 ); + Wln_GiaTransferNamesIfMatch( pGia, pGiaNames ); + if ( pGiaNames ) + Gia_ManStop( pGiaNames ); } else pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 ); From 66f5d7c7a2e4e199d08cee1ce1699b3905c7c733 Mon Sep 17 00:00:00 2001 From: Matt Liberty Date: Fri, 5 Jun 2026 06:05:32 +0000 Subject: [PATCH 10/13] mainUtils: match readline behavior when ABC_USE_READLINE is undefined The non-readline branch of Abc_UtilsGetUsersInput has three behavioral gaps versus the readline branch that break callers driving abc as a coprocess over a pipe (e.g. yosys's passes/techmap/abc.cc, which spawns "abc -s" with piped stdin/stdout and uses read_until_abc_done to wait for "abc NN> " lines): 1. The prompt is written with fprintf() and never flushed. On a pipe stdout is fully buffered, so the prompt never reaches the reader. The reader waits for the prompt, abc waits in fgets(), deadlock. 2. There is no echo of the line read from stdin. readline() emits each character to its output stream; yosys's protocol depends on seeing "abc NN> source ...\n" in the output to advance state. Without an echo it waits forever. 3. EOF on stdin is silently ignored: fgets() returns NULL but the function returns a stale Prompt buffer, causing a tight loop on pipe close. The readline branch exit(0)s on NULL. Fix all three. Echo only when stdin is not a tty -- on a tty the kernel already echoes typed characters during cooked input, so double-echo would be visible to interactive users. Signed-off-by: Matt Liberty --- src/base/main/mainUtils.c | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index 654d246f0..c1c67049a 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -18,6 +18,8 @@ ***********************************************************************/ +#include + #include "base/abc/abc.h" #include "mainInt.h" @@ -91,7 +93,13 @@ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc ) { char * pRetValue; fprintf( pAbc->Out, "%s", Prompt ); + fflush( pAbc->Out ); pRetValue = fgets( Prompt, 5000, stdin ); + if ( pRetValue == NULL ) { exit(0); } + if ( !isatty( fileno(stdin) ) ) { + fputs( Prompt, pAbc->Out ); + fflush( pAbc->Out ); + } return Prompt; } #endif From b7ee7a5f70c37e0b0cb00bde1bacfb8c26adf82a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 5 Jun 2026 16:15:34 +0700 Subject: [PATCH 11/13] Fix a windows compile problem. --- src/base/main/mainUtils.c | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index c1c67049a..5db012cfe 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -18,7 +18,11 @@ ***********************************************************************/ +#ifdef WIN32 +#include +#else #include +#endif #include "base/abc/abc.h" #include "mainInt.h" From 9749046cd6070b8796243e60af5e5b08419f6644 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 8 Jun 2026 17:05:54 +0700 Subject: [PATCH 12/13] Bug fix in required time propagation. --- src/map/if/ifTime.c | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 81f88fd72..73a5d8246 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -338,7 +338,7 @@ float If_ManDelayMax( If_Man_t * p, int fSeq ) void If_ManComputeRequired( If_Man_t * p ) { If_Obj_t * pObj; - int i, Counter; + int i, iBox, Counter; float reqTime; // compute area, clean required times, collect nodes used in the mapping @@ -480,7 +480,7 @@ void If_ManComputeRequired( If_Man_t * p ) if ( p->pPars->pTimesReq ) { Counter = 0; - If_ManForEachCo( p, pObj, i ) + If_ManForEachPo( p, pObj, i ) { reqTime = p->pPars->pTimesReq[i]; if ( If_ObjArrTime(If_ObjFanin0(pObj)) > reqTime + p->fEpsilon ) @@ -551,6 +551,9 @@ void If_ManComputeRequired( If_Man_t * p ) { reqTime = pObj->Required; Tim_ManSetCiRequired( p->pManTim, pObj->IdPio, reqTime ); + iBox = Tim_ManBoxForCi( p->pManTim, pObj->IdPio ); + if ( iBox >= 0 ) + Tim_ManSetPreviousTravIdBoxInputs( p->pManTim, iBox ); } else if ( If_ObjIsCo(pObj) ) { From 59896d6ec81ad8c2e5eaf9fce7d66e6ec2eba81f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 8 Jun 2026 17:45:17 +0700 Subject: [PATCH 13/13] Another bug fix in delay propagation. --- src/map/if/ifMap.c | 19 ++++++++++++++----- src/map/if/ifTime.c | 4 ++-- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index f93b73edb..6a0148d4f 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -194,7 +194,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL ); else if ( p->pPars->fDsdBalance ) pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL ); - else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell ) + else if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { int iLeaf, Intrinsic[IF_MAX_LUTSIZE]; float Delay = -IF_FLOAT_LARGE; @@ -364,7 +364,7 @@ IfMapBestCutDone: for ( iLeaf = 0; iLeaf < p->nCutLeavesCur; iLeaf++ ) { If_Obj_t * pLeaf = If_CutLeaf( p, pCut, iLeaf ); - if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && pCut->nLeaves > 1 ) + if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib && pCut->nLeaves > 1 ) { If_Cut_t * pBestCut = If_ObjCutBest( pLeaf ); assert( pBestCut != NULL ); @@ -472,8 +472,10 @@ IfMapBestCutDone: pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL ); else if ( p->pPars->fDsdBalance ) pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL ); - else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell ) + else if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { + int iLeaf, Intrinsic[IF_MAX_LUTSIZE]; + float Delay = -IF_FLOAT_LARGE; if ( pCut->nLeaves == 0 ) { pCut->Delay = 0.0; @@ -487,9 +489,16 @@ IfMapBestCutDone: pCut->fUseless = 0; goto IfMapCutEvalDone; } - assert( pCut->fUseless || p->fCutDelayCurValid ); assert( pCut->fUseless || pCut->Config != 0 ); - pCut->Delay = pCut->fUseless ? IF_FLOAT_LARGE : p->CutDelayCur; + if ( pCut->fUseless ) + pCut->Delay = IF_FLOAT_LARGE; + else + { + If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic ); + If_CutForEachLeaf( p, pCut, pLeaf, iLeaf ) + Delay = IF_MAX( Delay, If_ObjArrTime(pLeaf) + (float)Intrinsic[iLeaf] ); + pCut->Delay = Delay; + } IfMapCutEvalDone: ; } diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 73a5d8246..3126b75a7 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -131,7 +131,7 @@ float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut ) } else { - if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib ) + if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { int Intrinsic[IF_MAX_LUTSIZE]; if ( pCut->nLeaves == 0 ) @@ -233,7 +233,7 @@ void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, fl } else { - if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib ) + if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { int Intrinsic[IF_MAX_LUTSIZE]; if ( pCut->nLeaves == 0 )