From 3285adaf3220974e859ebc54349d9f2889af9a04 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Feb 2026 07:04:50 -0800 Subject: [PATCH 01/17] Updating &sprove to run %ufar. --- src/base/abci/abc.c | 55 +++++++++++++++++++++++++------ src/opt/ufar/UfarCmd.cpp | 38 ++++++++++++++++++++++ src/opt/ufar/UfarCmd.h | 3 ++ src/opt/ufar/UfarMgr.cpp | 39 +++++++++++++++++++--- src/opt/ufar/UfarMgr.h | 2 ++ src/opt/untk/NtkNtk.cpp | 20 +++++++++--- src/opt/untk/NtkNtk.h | 4 +-- src/proof/cec/cecProve.c | 70 +++++++++++++++++++++++++++++----------- 8 files changed, 192 insertions(+), 39 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 077c88d9b..5cb503463 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51320,10 +51320,15 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ); - int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; + typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; + typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; + extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); + extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); + Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL; + Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc; + int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWsvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF ) { switch ( c ) { @@ -51371,6 +51376,9 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nTimeOut3 <= 0 ) goto usage; break; + case 'u': + fUseUif ^= 1; + break; case 's': fSilent ^= 1; break; @@ -51386,27 +51394,56 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pAbc->pGia == NULL ) + if ( fUseUif ) + { + pGiaUse = NULL; + if ( pWlc == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no word-level design for option \"-u\".\n" ); + return 1; + } + pGiaTemp = Wlc_NtkBitBlast( pWlc, NULL ); + if ( pGiaTemp == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): Word-level bit-blasting has failed.\n" ); + return 1; + } + if ( (Gia_ManPoNum(pGiaTemp) & 1) == 1 ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): Internal \"&miter -x\" requires even number of bit-level outputs.\n" ); + Gia_ManStop( pGiaTemp ); + return 1; + } + pGiaUse = Gia_ManTransformMiter2( pGiaTemp ); + Gia_ManStop( pGiaTemp ); + pGiaTemp = NULL; + } + if ( pGiaUse == NULL ) { Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" ); return 1; } - if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + if ( Gia_ManRegNum(pGiaUse) == 0 ) { Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" ); + if ( fUseUif ) + Gia_ManStop( pGiaUse ); return 1; } - pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fVerbose, fVeryVerbose, fSilent ); - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + pAbc->Status = Cec_GiaProveTest( pGiaUse, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fUseUif, pWlc, fVerbose, fVeryVerbose, fSilent ); + Abc_FrameReplaceCex( pAbc, &pGiaUse->pCexSeq ); + if ( fUseUif ) + Gia_ManStop( pGiaUse ); return 0; usage: - Abc_Print( -2, "usage: &sprove [-PTUW num] [-svwh]\n" ); + Abc_Print( -2, "usage: &sprove [-PTUW num] [-usvwh]\n" ); Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes [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 : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut2 ); - Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); + Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); + 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" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp index 5bedeeca6..37728b04d 100755 --- a/src/opt/ufar/UfarCmd.cpp +++ b/src/opt/ufar/UfarCmd.cpp @@ -48,6 +48,44 @@ void Ufar_Init(Abc_Frame_t *pAbc) //Cmd_CommandAdd( pAbc, "Word level Prove", "%%miter", Abc_CommandCreateMiter, 0 ); } +int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId ) +{ + UFAR::UfarManager manager; + timeval t1; + set set_op_types; + Wlc_Ntk_t * pUse = pNtk; + int RetValue = -1; + if ( pNtk == NULL ) + return -1; + if ( Wlc_NtkPoNum(pUse) == 2 ) + { + pUse = UFAR::CreateMiter( pUse, 0 ); + if ( pUse == NULL ) + return -1; + } + else if ( Wlc_NtkPoNum(pUse) != 1 ) + return -1; + set_op_types.insert( WLC_OBJ_ARI_MULTI ); + if ( !UFAR::HasOperator( pUse, set_op_types ) ) + { + if ( pUse != pNtk ) + Wlc_NtkFree( pUse ); + return -1; + } + manager.params = UFAR::UfarManager::Params(); + manager.params.RunId = RunId; + manager.params.pFuncStop = pFuncStop; + if ( nTimeOut > 0 ) + manager.params.nTimeout = nTimeOut; + manager.params.iVerbosity = fVerbose ? 1 : 0; + gettimeofday( &t1, NULL ); + manager.Initialize( pUse, set_op_types ); + RetValue = manager.PerformUIFProve( t1 ); + if ( pUse != pNtk ) + Wlc_NtkFree( pUse ); + return RetValue; +} + static int Abc_CommandCreateMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNew = UFAR::CreateMiter(Wlc_AbcGetNtk(pAbc), 0); diff --git a/src/opt/ufar/UfarCmd.h b/src/opt/ufar/UfarCmd.h index d2b775269..52dfc8bb8 100755 --- a/src/opt/ufar/UfarCmd.h +++ b/src/opt/ufar/UfarCmd.h @@ -14,6 +14,9 @@ ABC_NAMESPACE_HEADER_START void Ufar_Init(Abc_Frame_t *pAbc); +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId ); + ABC_NAMESPACE_HEADER_END #endif /* SRC_EXT2_UIF_UIFCMD_H_ */ diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp index 67b5aed85..6973f69fb 100755 --- a/src/opt/ufar/UfarMgr.cpp +++ b/src/opt/ufar/UfarMgr.cpp @@ -819,8 +819,8 @@ void CexUifPairFinder::ComputeCoreUifPairs(const set& set_candidates, } void CexUifPairFinder::FindUifPairsBasic(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs) { - assert(Wlc_NtkPoNum(_pOrigNtk) == 1); - assert(Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) == 1); + if ( Wlc_NtkPoNum(_pOrigNtk) != 1 || Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) != 1 ) + return; _inputs.clear(); _outputs.clear(); @@ -879,8 +879,8 @@ void CexUifPairFinder::FindUifPairsBasic(const VecVecChar& cex_po_values, unsign } void CexUifPairFinder::FindUifPairs(const VecVecChar& cex_po_values, unsigned nLookBack, set& set_new_pairs) { - assert(Wlc_NtkPoNum(_pOrigNtk) == 1); - assert(Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) == 1); + if ( Wlc_NtkPoNum(_pOrigNtk) != 1 || Wlc_ObjRange(Wlc_NtkPo(_pOrigNtk, 0)) != 1 ) + return; _compute_max_bw(); @@ -931,7 +931,14 @@ void CexUifPairFinder::FindUifPairs(const VecVecChar& cex_po_values, unsigned nL } +static inline int Ufar_ShouldStop( const UfarManager::Params & p ) +{ + return p.pFuncStop && p.pFuncStop( p.RunId ); +} + UfarManager::Params::Params() : + RunId(-1), + pFuncStop(NULL), fCexMin(true), fPbaUif(false), fLazySim(true), @@ -1359,8 +1366,14 @@ void UfarManager::DetermineWhiteBoxes(Abc_Cex_t * pCex) { int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) { timeval t1, t2; gettimeofday(&t1, NULL); + if ( Ufar_ShouldStop(params) ) + return -1; Wlc_Ntk_t * pCurrent = BuildCurrentAbstraction(); + if ( Ufar_ShouldStop(params) ) { + Wlc_NtkFree(pCurrent); + return -1; + } if(!params.fileAbs.empty()) Wlc_WriteVer(pCurrent, &((params.fileAbs + "_abs.v")[0u]), 0, 0); @@ -1376,7 +1389,7 @@ int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) { } } */ - ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout); + ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId); Wlc_NtkFree(pCurrent); gettimeofday(&t2, NULL); @@ -1428,6 +1441,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut); }; + if ( Ufar_ShouldStop(params) ) + return -1; if (!params.fileStatesIn.empty()) { _read_states(params.fileStatesIn); if (params.iExp != -1) _massage_state_b(); @@ -1435,6 +1450,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } if (!params.fLazySim && !params.simSetting.empty()) { + if ( Ufar_ShouldStop(params) ) + return -1; unsigned origSize = _set_uif_pairs.size(); LOG(1) << "Try using simulation to find UIF pairs"; _simulate(); @@ -1450,6 +1467,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { while(true) { while(true) { + if ( Ufar_ShouldStop(params) ) + return -1; if (params.fPbaCex && mem.pCex2) { if(mem.pCex) Abc_CexFree(mem.pCex); mem.pCex = mem.pCex2; @@ -1462,6 +1481,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } if (ret == 0) { // SAT + if ( Ufar_ShouldStop(params) ) + return -1; // GetOperatorsInCex(mem.pCex); if (verify_cex_on_original(_pOrigNtk, mem.pCex)) { PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names); @@ -1470,11 +1491,15 @@ int UfarManager::PerformUIFProve(const timeval& timer) { unsigned n_before = _set_uif_pairs.size(); FindUifPairsUsingCex(mem.pCex, &mem.pCex2); + if ( Ufar_ShouldStop(params) ) + return -1; if (n_before == _set_uif_pairs.size()) { LOG(1) << "No new UIF pair is found in CEX"; if(!params.simSetting.empty()) { + if ( Ufar_ShouldStop(params) ) + return -1; LOG(1) << "Try using simulation to find UIF pairs"; _simulate(); FindUifPairsUsingSim(); @@ -1485,6 +1510,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } if (params.nGrey) { + if ( Ufar_ShouldStop(params) ) + return -1; DetermineGreyness(mem.pCex); } @@ -1509,6 +1536,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } } + if ( Ufar_ShouldStop(params) ) + return -1; DetermineWhiteBoxes(mem.pCex); ++n_iter_wb; diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h index ad2f9c477..31b91ef40 100755 --- a/src/opt/ufar/UfarMgr.h +++ b/src/opt/ufar/UfarMgr.h @@ -60,6 +60,8 @@ class UfarManager { public: struct Params { Params(); + int RunId; + int (*pFuncStop)(int); bool fCexMin; bool fPbaUif; bool fLazySim; diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 0c74a4761..97625f8bb 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -1119,7 +1119,8 @@ Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor) assert(Wlc_NtkPoNum(pNtk) == 2); Wlc_Ntk_t *pNew = Wlc_NtkDupDfsSimple(pNtk); - Wlc_NtkTransferNames( pNew, pNtk ); + if ( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(pNtk) ) + Wlc_NtkTransferNames( pNew, pNtk ); Wlc_Obj_t *pOldPo0 = Wlc_NtkPo(pNew, 0); Wlc_Obj_t *pOldPo1 = Wlc_NtkPo(pNew, 1); @@ -1145,7 +1146,8 @@ Wlc_Ntk_t * CreateMiter(Wlc_Ntk_t *pNtk, bool fXor) Wlc_NtkObj(pNew, iOldPo1)->fIsPo = 0; Wlc_Ntk_t *pNewNew = Wlc_NtkDupDfsSimple(pNew); - Wlc_NtkTransferNames( pNewNew, pNew ); + if ( !Wlc_NtkHasNameId(pNewNew) && Wlc_NtkHasNameId(pNew) ) + Wlc_NtkTransferNames( pNewNew, pNew ); Wlc_NtkFree(pNew); return pNewNew; } @@ -1245,9 +1247,11 @@ static void readCexFromFile(int& ret, FILE * file, Abc_Cex_t ** ppCex, int nOrig } } -int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout) { +int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, struct timespec * timeout, int (*pFuncStop)(int), int RunId) { + if ( pFuncStop && pFuncStop(RunId) ) + return -1; if ( !pParSetting || pParSetting->empty() || Wlc_NtkFfNum(pNtk) == 0 ) - return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn ); + return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId ); if(*ppCex) { Abc_CexFree(*ppCex); @@ -1262,11 +1266,15 @@ int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, ret = RunConcurrentSolver( pNtk, parSolvers, ppCex, timeout ); + if ( pFuncStop && pFuncStop(RunId) ) + return -1; return ret; } -int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn) { +int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, const string* pParSetting, bool fSyn, int (*pFuncStop)(int), int RunId) { + if ( pFuncStop && pFuncStop(RunId) ) + return -1; if(*ppCex) { Abc_CexFree(*ppCex); *ppCex = NULL; @@ -1303,6 +1311,8 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam Pdr_Par_t PdrPars, *pPdrPars = &PdrPars; Pdr_ManSetDefaultParams(pPdrPars); pPdrPars->nConfLimit = 0; + pPdrPars->RunId = RunId; + pPdrPars->pFuncStop = pFuncStop; //pPdrPars->fDumpInv = 1; Abc_FrameReadGlobalFrame()->pNtkCur = pAbcNtk; int res = Abc_NtkDarPdr(pAbcNtk, pPdrPars); diff --git a/src/opt/untk/NtkNtk.h b/src/opt/untk/NtkNtk.h index e3323f123..85d9ac935 100755 --- a/src/opt/untk/NtkNtk.h +++ b/src/opt/untk/NtkNtk.h @@ -136,8 +136,8 @@ void PrintWordCEX(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex, const std::vectorfSolved != 0; +} static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) { Par_ThData_t * pThData = (Par_ThData_t *)pUser; @@ -114,6 +126,12 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par { abctime clk = Abc_Clock(); int RetValue = -1; + if ( iEngine != PAR_ENGINE_UFAR && Gia_ManRegNum(p) == 0 ) + { + if ( fVerbose ) + printf( "Engine %d skipped because the current miter is combinational.\n", iEngine ); + return -1; + } //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock(); if ( fVerbose ) printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut ); @@ -212,6 +230,15 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } RetValue = Bmcg_ManPerform( p, pPars ); } + else if ( iEngine == PAR_ENGINE_UFAR ) + { + if ( pThData && pThData->pWlc ) + { + g_pUfarShare = pThData->pShare; + RetValue = Ufar_ProveWithTimeout( pThData->pWlc, pThData->nTimeOutU, fVerbose, Cec_SProveStopUfar, 0 ); + g_pUfarShare = NULL; + } + } else assert( 0 ); //while ( Abc_Clock() < clkStop ); if ( pThData && pThData->pShare && RetValue != -1 ) @@ -224,6 +251,8 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) { + if ( Gia_ManRegNum(p) == 0 ) + return Gia_ManDup( p ); Ssw_Pars_t Pars, * pPars = &Pars; Ssw_ManSetDefaultParams( pPars ); Aig_Man_t * pAig = Gia_ManToAigSimple( p ); @@ -235,6 +264,8 @@ Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) } Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) { + if ( Gia_ManRegNum(p) == 0 ) + return Gia_ManDup( p ); Cec_ParCor_t Pars, * pPars = &Pars; Cec_ManCorSetDefaultParams( pPars ); pPars->nBTLimit = 100; @@ -275,34 +306,36 @@ void * Cec_GiaProveWorkerThread( void * pArg ) assert( 0 ); return NULL; } -void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare ) +void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fUseUif, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare ) { int i, status; - assert( nProcs <= PAR_THR_MAX ); - for ( i = 0; i < nProcs; i++ ) + assert( nWorkers <= PAR_THR_MAX ); + for ( i = 0; i < nWorkers; i++ ) { ThData[i].p = Gia_ManDup(p); - ThData[i].iEngine = i; + ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i; ThData[i].nTimeOut = nTimeOut; ThData[i].fWorking = 0; ThData[i].Result = -1; ThData[i].fVerbose = fVerbose; + ThData[i].nTimeOutU= nTimeOutU; + ThData[i].pWlc = pWlc; ThData[i].pShare = pShare; if ( !WorkerThread ) continue; status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 ); } - for ( i = 0; i < nProcs; i++ ) + for ( i = 0; i < nWorkers; i++ ) ThData[i].fWorking = 1; } -int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int RetValue, int * pRetEngine ) +int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine ) { int i; - for ( i = 0; i < nProcs; i++ ) + for ( i = 0; i < nWorkers; i++ ) { if ( RetValue == -1 && !ThData[i].fWorking && ThData[i].Result != -1 ) { RetValue = ThData[i].Result; - *pRetEngine = i; + *pRetEngine = ThData[i].iEngine; if ( !p->pCexSeq && ThData[i].p->pCexSeq ) p->pCexSeq = Abc_CexDup( ThData[i].p->pCexSeq, -1 ); } @@ -312,13 +345,13 @@ int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int Re return RetValue; } -int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ) { abctime clkScorr = 0, clkTotal = Abc_Clock(); Par_ThData_t ThData[PAR_THR_MAX]; pthread_t WorkerThread[PAR_THR_MAX]; Par_Share_t Share; - int i, RetValue = -1, RetEngine = -2; + int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -2; memset( &Share, 0, sizeof(Par_Share_t) ); Abc_CexFreeP( &p->pCexComb ); Abc_CexFreeP( &p->pCexSeq ); @@ -329,7 +362,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in fflush( stdout ); assert( nProcs == 3 || nProcs == 5 ); - Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread, &Share ); + assert( nWorkers <= PAR_THR_MAX ); + Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share ); // meanwhile, perform scorr Gia_Man_t * pScorr = Cec_GiaScorrNew( p ); @@ -337,7 +371,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in if ( Gia_ManAndNum(pScorr) == 0 ) RetValue = 1, RetEngine = -1; - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) { abctime clkScorr2, clkStart = Abc_Clock(); @@ -345,7 +379,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(p), Gia_ManAndNum(pScorr) ); Abc_PrintTime( 1, "Time", clkScorr ); } - Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL, &Share ); + Cec_GiaInitThreads( ThData, nWorkers, pScorr, nTimeOut2, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); // meanwhile, perform scorr if ( Gia_ManAndNum(pScorr) < 100000 ) @@ -355,16 +389,16 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in if ( Gia_ManAndNum(pScorr2) == 0 ) RetValue = 1; - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) { if ( !fSilent && fVerbose ) { printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) ); Abc_PrintTime( 1, "Time", clkScorr2 ); } - Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL, &Share ); + Cec_GiaInitThreads( ThData, nWorkers, pScorr2, nTimeOut3, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine ); + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); // do something else } Gia_ManStop( pScorr2 ); @@ -373,7 +407,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Gia_ManStop( pScorr ); // stop threads - for ( i = 0; i < nProcs; i++ ) + for ( i = 0; i < nWorkers; i++ ) { ThData[i].p = NULL; ThData[i].fWorking = 1; From 2726f0e470b79b787a52df05ee45a987c95f4b6a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Feb 2026 07:12:50 -0800 Subject: [PATCH 02/17] Fixing compiler problem. --- src/base/abci/abc.c | 9 +++++---- src/base/wlc/wlcBlast.c | 9 ++++----- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5cb503463..9114016ec 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -680,6 +680,11 @@ extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk ); extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut ); +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; +extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); +extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -51320,10 +51325,6 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; - typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; - extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); - extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL; Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc; int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index f028a1324..495861d90 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1722,7 +1722,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) Wlc_ObjForEachFanin( pObj, iFanin, k ) if ( k > 0 ) fSigned &= Wlc_NtkObj(p, iFanin)->Signed; - if ( pParIn->fBlastNew && nRange0 <= 16 ) + if ( pPar->fBlastNew && nRange0 <= 16 ) { char * pNums = Wlc_NtkMuxTreeString( nRange0 ); Vec_Int_t ** pvDecs = Wlc_NtkMuxTree3DecsDerive( pNew, pFans0, nRange0, pNums ); @@ -1989,9 +1989,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU); if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 ); if ( fSigned ) - iLit = pParIn->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax ); + iLit = pPar->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax ); else - iLit = pParIn->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax ); + iLit = pPar->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax ); iLit = Abc_LitNotCond( iLit, fCompl ); Vec_IntFill( vRes, 1, iLit ); for ( k = 1; k < nRange; k++ ) @@ -2124,7 +2124,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) else if ( pObj->Type == WLC_OBJ_DEC ) { int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 ); - if ( pParIn->fBlastNew ) + if ( pPar->fBlastNew ) Wlc_BlastDecoder2( pNew, pArg0, nRange0, vTemp2, vRes ); else Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes ); @@ -3015,4 +3015,3 @@ void Wlc_MultBlastTest() ABC_NAMESPACE_IMPL_END - From 8475386dfa921e6337d312f0b37e4eac47d02bf6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Feb 2026 09:52:37 -0800 Subject: [PATCH 03/17] Making %ufar preserve AIG name. --- src/base/wlc/wlcBlast.c | 2 +- src/opt/ufar/UfarMgr.cpp | 14 ++++++++++++++ src/opt/ufar/UfarPth.cpp | 26 ++++++++++++++++++++++++++ src/opt/untk/NtkNtk.cpp | 21 ++++++++++++++++----- src/proof/cec/cecProve.c | 28 +++++++++++++++++++++++++++- 5 files changed, 84 insertions(+), 7 deletions(-) diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 495861d90..7e90863d8 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1434,6 +1434,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) // create AIG manager pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 ); pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->fGiaSimple = pPar->fGiaSimple; if ( !pPar->fGiaSimple ) Gia_ManHashAlloc( pNew ); @@ -2730,7 +2731,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) Abc_FrameSetLibBox( pBoxLib ); } - //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName ); // dump the miter parts if ( 0 ) { diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp index 6973f69fb..45487af77 100755 --- a/src/opt/ufar/UfarMgr.cpp +++ b/src/opt/ufar/UfarMgr.cpp @@ -981,6 +981,10 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set& types) { profile = Profile(); _pOrigNtk = Wlc_NtkDupDfsSimple(pNtk); + if ( _pOrigNtk->pName == NULL ) + _pOrigNtk->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec ); + if ( _pOrigNtk->pSpec == NULL ) + _pOrigNtk->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec ); Wlc_Obj_t * pObj; int i; @@ -1083,6 +1087,16 @@ Wlc_Ntk_t * UfarManager::BuildCurrentAbstraction() { pNew = RemoveAuxPOs(pTemp = pNew, Wlc_NtkPoNum(_pOrigNtk)); Wlc_NtkFree(pTemp); + // Preserve benchmark identity through abstraction refinements so + // downstream bit-level engines report a meaningful miter name. + if ( _pOrigNtk ) + { + ABC_FREE( pNew->pName ); + ABC_FREE( pNew->pSpec ); + pNew->pName = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec ); + pNew->pSpec = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec ); + } + // Wlc_WriteVer(pNew, "Abs.v", 0, 0); return pNew; diff --git a/src/opt/ufar/UfarPth.cpp b/src/opt/ufar/UfarPth.cpp index 85bb0e178..c6f8fd276 100755 --- a/src/opt/ufar/UfarPth.cpp +++ b/src/opt/ufar/UfarPth.cpp @@ -33,6 +33,28 @@ using namespace std; namespace UFAR { +static inline void Ufar_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig ) +{ + char * pName = pGia->pName ? pGia->pName : pGia->pSpec; + if ( pName == NULL ) + return; + if ( pAig->pName == NULL ) + pAig->pName = Abc_UtilStrsav( pName ); + if ( pAig->pSpec == NULL ) + pAig->pSpec = Abc_UtilStrsav( pName ); +} + +static inline void Ufar_CopyAigNameToNtk( Aig_Man_t * pAig, Abc_Ntk_t * pNtk ) +{ + char * pName = pAig->pName ? pAig->pName : pAig->pSpec; + if ( pName == NULL ) + return; + if ( pNtk->pName == NULL ) + pNtk->pName = Abc_UtilStrsav( pName ); + if ( pNtk->pSpec == NULL ) + pNtk->pSpec = Abc_UtilStrsav( pName ); +} + // mutext to control access to shared variables pthread_mutex_t g_mutex; // cv to control timer @@ -63,6 +85,7 @@ class PDR : public Solver { Pth_Data_t * pData = (Pth_Data_t *)pArg; _pAig = Gia_ManToAigSimple( pData->pGia ); + Ufar_CopyGiaNameToAig( pData->pGia, _pAig ); Pdr_Par_t * pPdrPars = &_PdrPars; Pdr_ManSetDefaultParams(pPdrPars); @@ -93,6 +116,7 @@ class PDRA : public Solver { Pth_Data_t * pData = (Pth_Data_t *)pArg; _pAig = Gia_ManToAigSimple( pData->pGia ); + Ufar_CopyGiaNameToAig( pData->pGia, _pAig ); Pdr_Par_t * pPdrPars = &_PdrPars; Pdr_ManSetDefaultParams(pPdrPars); @@ -126,7 +150,9 @@ class BMC3 : public Solver { BMC3 ( void * pArg ) { Pth_Data_t * pData = (Pth_Data_t *)pArg; Aig_Man_t * pAig = Gia_ManToAigSimple( pData->pGia ); + Ufar_CopyGiaNameToAig( pData->pGia, pAig ); _pNtk = Abc_NtkFromAigPhase( pAig ); + Ufar_CopyAigNameToNtk( pAig, _pNtk ); Aig_ManStop( pAig ); Saig_ParBmc_t * pBmcPars = &_Pars; diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 97625f8bb..9c2a1da85 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -52,11 +52,14 @@ static inline int create_buffer(Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFa Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk) { Wlc_BstPar_t Par, * pPar = &Par; Wlc_BstParDefault( pPar ); - return Wlc_NtkBitBlast(pNtk, pPar); - //Gia_Man_t * pGia = Wlc_NtkBitBlast2(pNtk, NULL); - //printf( "Usingn old bit-blaster: " ); - //Gia_ManPrintStats( pGia, NULL ); - //return pGia; + Gia_Man_t * pGia = Wlc_NtkBitBlast(pNtk, pPar); + if ( pGia == NULL ) + return NULL; + if ( pGia->pName == NULL ) + pGia->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec ); + if ( pGia->pSpec == NULL ) + pGia->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec ); + return pGia; } template @@ -1292,7 +1295,15 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam } Aig_Man_t * pAig = Gia_ManToAig(pGia, 0); + if ( pAig->pName == NULL ) + pAig->pName = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec ); + if ( pAig->pSpec == NULL ) + pAig->pSpec = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec ); Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase(pAig); + if ( pAbcNtk->pName == NULL ) + pAbcNtk->pName = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec ); + if ( pAbcNtk->pSpec == NULL ) + pAbcNtk->pSpec = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec ); if (pFileName && !pFileName->empty()) Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u])); diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 3c0fd3df6..273791fe4 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -83,6 +83,26 @@ typedef struct Par_ThData_t_ Par_Share_t * pShare; } Par_ThData_t; static volatile Par_Share_t * g_pUfarShare = NULL; +static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst ) +{ + char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec; + if ( pName == NULL ) + return; + if ( pDst->pName == NULL ) + pDst->pName = Abc_UtilStrsav( pName ); + if ( pDst->pSpec == NULL ) + pDst->pSpec = Abc_UtilStrsav( pName ); +} +static inline void Cec_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig ) +{ + char * pName = pGia->pName ? pGia->pName : pGia->pSpec; + if ( pName == NULL ) + return; + if ( pAig->pName == NULL ) + pAig->pName = Abc_UtilStrsav( pName ); + if ( pAig->pSpec == NULL ) + pAig->pSpec = Abc_UtilStrsav( pName ); +} static int Cec_SProveStopUfar( int RunId ) { (void)RunId; @@ -161,6 +181,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par pPars->pProgress = (void *)pThData; } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Cec_CopyGiaNameToAig( p, pAig ); RetValue = Saig_ManBmcScalable( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); @@ -177,6 +198,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par pPars->pProgress = (void *)pThData; } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Cec_CopyGiaNameToAig( p, pAig ); RetValue = Pdr_ManSolve( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); @@ -194,6 +216,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par pPars->pProgress = (void *)pThData; } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Cec_CopyGiaNameToAig( p, pAig ); RetValue = Saig_ManBmcScalable( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); @@ -211,6 +234,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par pPars->pProgress = (void *)pThData; } Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + Cec_CopyGiaNameToAig( p, pAig ); RetValue = Pdr_ManSolve( pAig, pPars ); p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); @@ -313,6 +337,7 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int for ( i = 0; i < nWorkers; i++ ) { ThData[i].p = Gia_ManDup(p); + Cec_CopyGiaName( p, ThData[i].p ); ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i; ThData[i].nTimeOut = nTimeOut; ThData[i].fWorking = 0; @@ -414,7 +439,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in } if ( !fSilent ) { - printf( "Problem \"%s\" is ", p->pSpec ); + char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p); + printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" ); if ( RetValue == 0 ) printf( "SATISFIABLE (solved by %d).", RetEngine ); else if ( RetValue == 1 ) From 3cdb1c4c3b487e16662fe26fb730de18236244b3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Feb 2026 19:26:35 -0800 Subject: [PATCH 04/17] Dumping LUT-mapped networks in Vivado-readable Verilog. --- src/base/abc/abcHieGia.c | 215 ++++++++++++++++++++++++++++++++++++++- src/base/abci/abc.c | 27 ++++- 2 files changed, 238 insertions(+), 4 deletions(-) diff --git a/src/base/abc/abcHieGia.c b/src/base/abc/abcHieGia.c index 239f73ef1..f2f6f8ca6 100644 --- a/src/base/abc/abcHieGia.c +++ b/src/base/abc/abcHieGia.c @@ -1292,12 +1292,201 @@ static void GiaHie_DumpInterfaceAssigns( Gia_Man_t * p, char * pFileName ) fclose( pFile ); } +/**Function************************************************************* + + Synopsis [Dumps mapped AIG as LUT6 instances in Verilog] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName ) +{ + int i, k, iFanin, nLutSize, nDigits; + FILE * pFile; + Vec_Int_t * vLeaves; + word * pTruth; + Gia_Obj_t * pObj; + + // Check if AIG is mapped + if ( !Gia_ManHasMapping(p) ) + { + printf( "Cannot write LUT-based Verilog because AIG is not mapped.\n" ); + return; + } + + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileName ); + return; + } + + nDigits = Abc_Base10Log( Gia_ManObjNum(p) ); + if ( nDigits < 3 ) + nDigits = 3; + + // Write header + fprintf( pFile, "`timescale 1ns/1ps\n\n" ); + + // Write LUT module definitions for Yosys compatibility (compact version) + fprintf( pFile, "module LUT2 #( parameter INIT = 04\'h0 ) ( output O, input I0, I1 );\n" ); + fprintf( pFile, " assign O = INIT[ {I1, I0} ];\n" ); + fprintf( pFile, "endmodule\n" ); + + fprintf( pFile, "module LUT3 #( parameter INIT = 08\'h0 ) ( output O, input I0, I1, I2 );\n" ); + fprintf( pFile, " assign O = INIT[ {I2, I1, I0} ];\n" ); + fprintf( pFile, "endmodule\n" ); + + fprintf( pFile, "module LUT4 #( parameter INIT = 16\'h0 ) ( output O, input I0, I1, I2, I3 );\n" ); + fprintf( pFile, " assign O = INIT[ {I3, I2, I1, I0} ];\n" ); + fprintf( pFile, "endmodule\n" ); + + fprintf( pFile, "module LUT5 #( parameter INIT = 32\'h0 ) ( output O, input I0, I1, I2, I3, I4 );\n" ); + fprintf( pFile, " assign O = INIT[ {I4, I3, I2, I1, I0} ];\n" ); + fprintf( pFile, "endmodule\n" ); + + fprintf( pFile, "module LUT6 #( parameter INIT = 64\'h0 ) ( output O, input I0, I1, I2, I3, I4, I5 );\n" ); + fprintf( pFile, " assign O = INIT[ {I5, I4, I3, I2, I1, I0} ];\n" ); + fprintf( pFile, "endmodule\n\n" ); + + // Write main module + fprintf( pFile, "module " ); + GiaHie_DumpModuleName( pFile, p->pName ); + fprintf( pFile, " (\n" ); + GiaHie_DumpPortDecls( p, pFile ); + fprintf( pFile, "\n);\n\n" ); + + // Declare wires for inputs (using object IDs like regular &write_ver) + if ( Gia_ManCiNum(p) ) + { + fprintf( pFile, " wire " ); + GiaHie_WriteObjRange( pFile, p, 0, Gia_ManCiNum(p), nDigits, 7, 4, 0, 1 ); + fprintf( pFile, ";\n\n" ); + GiaHie_DumpInputAssigns( p, pFile, nDigits ); + fprintf( pFile, "\n" ); + } + + // Declare wires for outputs (using object IDs like regular &write_ver) + if ( Gia_ManCoNum(p) ) + { + fprintf( pFile, " wire " ); + GiaHie_WriteObjRange( pFile, p, 0, Gia_ManCoNum(p), nDigits, 7, 4, 0, 0 ); + fprintf( pFile, ";\n\n" ); + GiaHie_DumpOutputAssigns( p, pFile, nDigits ); + fprintf( pFile, "\n" ); + } + + // Declare internal wires for LUT outputs (10 per line) + { + int nWiresPerLine = 10; + int nWireCount = 0; + int fFirst = 1; + Gia_ManForEachLut( p, i ) + { + if ( nWireCount == 0 ) + fprintf( pFile, " wire " ); + if ( !fFirst ) + fprintf( pFile, ", " ); + fprintf( pFile, "n%0*d", nDigits, i ); + fFirst = 0; + nWireCount++; + if ( nWireCount == nWiresPerLine ) + { + fprintf( pFile, ";\n" ); + nWireCount = 0; + fFirst = 1; + } + } + if ( nWireCount > 0 ) + fprintf( pFile, ";\n" ); + } + fprintf( pFile, "\n" ); + + // Initialize truth table computation + vLeaves = Vec_IntAlloc( 6 ); + Gia_ObjComputeTruthTableStart( p, 6 ); + + // Write LUT6 instances + Gia_ManForEachLut( p, i ) + { + nLutSize = Gia_ObjLutSize( p, i ); + + // Collect LUT inputs + Vec_IntClear( vLeaves ); + Gia_LutForEachFanin( p, i, iFanin, k ) + Vec_IntPush( vLeaves, iFanin ); + + // Compute truth table + pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, i), vLeaves ); + + // Write LUT instance - use appropriate size LUT based on inputs + if ( nLutSize <= 1 ) + nLutSize = 2; // minimum LUT size is 2 + + // Determine INIT width and padding + int nInitBits = (1 << nLutSize); + unsigned long long truthValue = (nLutSize <= 6) ? pTruth[0] : 0; + + // Mask truth value to the appropriate number of bits + if ( nLutSize < 6 ) + truthValue &= ((1ULL << nInitBits) - 1); + + // Write LUT instance with padding for alignment + fprintf( pFile, " (* DONT_TOUCH = \"yes\" *) LUT%d #(", nLutSize ); + + // Write INIT parameter with appropriate width and padding aligned to 64-bit width + if ( nLutSize == 2 ) + fprintf( pFile, ".INIT(04'h%01llx )) u_lut%0*d (", truthValue, nDigits, i ); + else if ( nLutSize == 3 ) + fprintf( pFile, ".INIT(08'h%02llx )) u_lut%0*d (", truthValue, nDigits, i ); + else if ( nLutSize == 4 ) + fprintf( pFile, ".INIT(16'h%04llx )) u_lut%0*d (", truthValue, nDigits, i ); + else if ( nLutSize == 5 ) + fprintf( pFile, ".INIT(32'h%08llx )) u_lut%0*d (", truthValue, nDigits, i ); + else // nLutSize == 6 + fprintf( pFile, ".INIT(64'h%016llx)) u_lut%0*d (", truthValue, nDigits, i ); + + // Write LUT inputs - only the ones actually used by this LUT size + for ( k = 0; k < nLutSize; k++ ) + { + iFanin = Vec_IntEntry( vLeaves, k ); + if ( k > 0 ) + fprintf( pFile, ", " ); + fprintf( pFile, ".I%d(n%0*d)", k, nDigits, iFanin ); + } + + // Write LUT output + fprintf( pFile, ", .O(n%0*d));\n", nDigits, i ); + } + + // Cleanup truth table computation + Gia_ObjComputeTruthTableStop( p ); + Vec_IntFree( vLeaves ); + + fprintf( pFile, "\n" ); + + // Connect internal nodes to outputs (like regular &write_ver) + Gia_ManForEachCo( p, pObj, i ) + { + fprintf( pFile, " assign n%0*d = ", nDigits, Gia_ManCoIdToId(p, i) ); + GiaHie_PrintObjLit( pFile, Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj), nDigits ); + fprintf( pFile, ";\n" ); + } + + fprintf( pFile, "\nendmodule\n" ); + fclose( pFile ); +} + /**Function************************************************************* Synopsis [] Description [] - + SideEffects [] SeeAlso [] @@ -1314,6 +1503,30 @@ void Gia_WriteVerilog( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fV GiaHie_DumpInterfaceAssigns( pGia, pFileName ); } +/**Function************************************************************* + + Synopsis [Writes mapped AIG as LUT6-based Verilog] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_WriteMappedVerilog( char * pFileName, Gia_Man_t * pGia, int fVerbose ) +{ + (void)fVerbose; + if ( pFileName == NULL || pGia == NULL ) + return; + if ( !Gia_ManHasMapping(pGia) ) + { + printf( "Cannot write LUT-based Verilog because AIG is not mapped.\n" ); + return; + } + GiaHie_DumpMappedLuts( pGia, pFileName ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9114016ec..dbb5ed99e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35109,15 +35109,17 @@ usage: int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_WriteVerilog( char * pFileName, Gia_Man_t * pGia, int fUseGates, int fVerbose ); + extern void Gia_WriteMappedVerilog( char * pFileName, Gia_Man_t * pGia, int fVerbose ); char * pFileSpec = NULL; Abc_Ntk_t * pNtkSpec = NULL; char * pFileName; char ** pArgvNew; int c, nArgcNew; int fUseGates = 0; + int fUseLuts = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Sgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Sglvh" ) ) != EOF ) { switch ( c ) { @@ -35133,6 +35135,9 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': fUseGates ^= 1; break; + case 'l': + fUseLuts ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -35157,7 +35162,21 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "There is no AIG to write.\n" ); return 1; } - Gia_WriteVerilog( pFileName, pAbc->pGia, fUseGates, fVerbose ); + // Check if we should write LUT-based Verilog + if ( fUseLuts || (Gia_ManHasMapping(pAbc->pGia) && !fUseGates) ) + { + if ( !Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "Cannot write LUT-based Verilog because AIG is not mapped.\n" ); + Abc_Print( -1, "Use \"&if\" to map the AIG first, or omit the -l flag.\n" ); + return 1; + } + Gia_WriteMappedVerilog( pFileName, pAbc->pGia, fVerbose ); + } + else + { + Gia_WriteVerilog( pFileName, pAbc->pGia, fUseGates, fVerbose ); + } } else { @@ -35179,13 +35198,15 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &write_ver [-S ] [-gvh] \n" ); + Abc_Print( -2, "usage: &write_ver [-S ] [-glvh] \n" ); Abc_Print( -2, "\t writes hierarchical Verilog\n" ); Abc_Print( -2, "\t-S file : file name for the original design (required when hierarchy is present)\n" ); Abc_Print( -2, "\t-g : toggle output gates vs assign-statements [default = %s]\n", fUseGates? "gates": "assigns" ); + Abc_Print( -2, "\t-l : write LUT6-based Verilog for mapped AIGs [default = %s]\n", fUseLuts? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the file name\n"); + Abc_Print( -2, "\tNote: When AIG is mapped and -l is not specified, LUT-based output is automatically used.\n"); return 1; } From 62d05a883257005be93cf9a872ac24b10f2e0b88 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Feb 2026 10:01:16 -0800 Subject: [PATCH 05/17] Enable ccache in Makefile. --- Makefile | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Makefile b/Makefile index a9d9b79c5..eeff20d24 100644 --- a/Makefile +++ b/Makefile @@ -4,6 +4,13 @@ CXX := g++ AR := ar LD := $(CXX) +# Auto-enable ccache if available +CCACHE := $(shell command -v ccache 2>/dev/null) +ifneq ($(CCACHE),) + CC := $(CCACHE) $(CC) + CXX := $(CCACHE) $(CXX) +endif + MSG_PREFIX ?= ABCSRC ?= . VPATH = $(ABCSRC) @@ -219,6 +226,7 @@ clean: $(VERBOSE)rm -rvf $(OBJ) $(VERBOSE)rm -rvf $(GARBAGE) $(VERBOSE)rm -rvf $(OBJ:.o=.d) + @if [ -n "$(CCACHE)" ]; then echo "$(MSG_PREFIX)ccache available: $(CCACHE)"; fi tags: etags `find . -type f -regex '.*\.\(c\|h\)'` From 3dd086febe43d0d2cd2ab945d7247be54abe991d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Feb 2026 10:02:42 -0800 Subject: [PATCH 06/17] New command ÷, etc. --- src/aig/gia/giaDup.c | 120 +++++++++++++++++++++++++++++++++++++ src/base/abc/abcHieGia.c | 4 +- src/base/abci/abc.c | 122 ++++++++++++++++++++++++++++++++++++-- src/base/abci/abcVerify.c | 27 +++++++-- 4 files changed, 262 insertions(+), 11 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 0c0fd3d1e..ba0b7d78c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -23,6 +23,7 @@ #include "misc/vec/vecWec.h" #include "proof/cec/cec.h" #include "misc/util/utilTruth.h" +#include "misc/extra/extra.h" ABC_NAMESPACE_IMPL_START @@ -6844,6 +6845,125 @@ Gia_Man_t * Gia_ManDupExtractMffc( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * return pNew; } +/**Function************************************************************* + + Synopsis [Divides the AIG into 2 parts at middle level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel ) +{ + Gia_Man_t * pPart0, * pPart1; + Gia_Obj_t * pObj; + Vec_Int_t * vCutNodes; + Vec_Ptr_t * vCutNames; + char * pFileName; + int i, Lcut; + assert( nParts == 2 ); + + // Use specified cut level or default to middle + if ( nCutLevel > 0 ) + Lcut = nCutLevel; + else + Lcut = Gia_ManLevelNum(p) / 2; + printf( "Dividing at level %d (total levels = %d). ", Lcut, Gia_ManLevelNum(p) ); + + // mark the nodes pointed to under the cut + Gia_ManForEachAnd( p, pObj, i ) { + if ( Gia_ObjLevel(p, pObj) <= Lcut ) + continue; + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) <= Lcut ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + if ( Gia_ObjLevel(p, Gia_ObjFanin1(pObj)) <= Lcut ) + Gia_ObjFanin1(pObj)->fMark0 = 1; + } + Gia_ManForEachCo( p, pObj, i ) + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pObj)) < Lcut ) + Gia_ObjFanin0(pObj)->fMark0 = 1; + + // Collect nodes at the cut (nodes at level Lcut that are needed by upper levels) + vCutNodes = Vec_IntAlloc( 100 ); + Gia_ManForEachObj1( p, pObj, i ) { + if ( !pObj->fMark0 ) + continue; + pObj->fMark0 = 0; + Vec_IntPush( vCutNodes, i ); + } + printf( "Found %d nodes at the cut\n", Vec_IntSize(vCutNodes) ); + + // Create names for cut nodes + vCutNames = Vec_PtrAlloc( Vec_IntSize(vCutNodes) ); + for ( i = 0; i < Vec_IntSize(vCutNodes); i++ ) { + char Buffer[100]; sprintf( Buffer, "cut[%d]", i ); + Vec_PtrPush( vCutNames, Abc_UtilStrsav(Buffer) ); + } + + // Create Part 0 (bottom part: levels 0 to Lcut) + pPart0 = Gia_ManStart( Gia_ManObjNum(p) ); + pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part0" ); + pPart0->pName = Abc_UtilStrsav( pFileName ); + pPart0->pSpec = Abc_UtilStrsav( pFileName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pPart0 ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjLevel(p, pObj) <= Lcut ) + pObj->Value = Gia_ManAppendAnd( pPart0, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vCutNodes, p, pObj, i ) + Gia_ManAppendCo( pPart0, pObj->Value ); + + // Add names to Part 0 + if ( p->vNamesIn ) { + pPart0->vNamesIn = Vec_PtrDupStr( p->vNamesIn ); + pPart0->vNamesOut = Vec_PtrDupStr( vCutNames ); + } + + // Write Part 0 + pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part0.aig" ); + Gia_AigerWrite( pPart0, pFileName, 0, 0, 0 ); + printf( "Part 0: PI = %d, PO = %d, AND = %d, written to %s\n", + Gia_ManCiNum(pPart0), Gia_ManCoNum(pPart0), Gia_ManAndNum(pPart0), pFileName ); + Gia_ManStop( pPart0 ); + + // Create Part 1 (top part: levels > Lcut) + pPart1 = Gia_ManStart( Gia_ManObjNum(p) ); + pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part1" ); + pPart1->pName = Abc_UtilStrsav( pFileName ); + pPart1->pSpec = Abc_UtilStrsav( pFileName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObjVec( vCutNodes, p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pPart1 ); + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjLevel(p, pObj) > Lcut ) + pObj->Value = Gia_ManAppendAnd( pPart1, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pPart1, Gia_ObjFanin0Copy(pObj) ); + + // Add names to Part 1 + if ( p->vNamesOut ) { + pPart1->vNamesIn = Vec_PtrDupStr( vCutNames ); + pPart1->vNamesOut = Vec_PtrDupStr( p->vNamesOut ); + } + + // Write Part 1 + pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part1.aig" ); + Gia_AigerWrite( pPart1, pFileName, 0, 0, 0 ); + printf( "Part 1: PI = %d, PO = %d, AND = %d, written to %s\n", + Gia_ManCiNum(pPart1), Gia_ManCoNum(pPart1), Gia_ManAndNum(pPart1), pFileName ); + Gia_ManStop( pPart1 ); + + // Clean up + Vec_IntFree( vCutNodes ); + Vec_PtrFreeFree( vCutNames ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcHieGia.c b/src/base/abc/abcHieGia.c index f2f6f8ca6..ea3c2d09a 100644 --- a/src/base/abc/abcHieGia.c +++ b/src/base/abc/abcHieGia.c @@ -1333,6 +1333,7 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName ) fprintf( pFile, "`timescale 1ns/1ps\n\n" ); // Write LUT module definitions for Yosys compatibility (compact version) + fprintf( pFile, "`ifdef LUTSPECS\n" ); fprintf( pFile, "module LUT2 #( parameter INIT = 04\'h0 ) ( output O, input I0, I1 );\n" ); fprintf( pFile, " assign O = INIT[ {I1, I0} ];\n" ); fprintf( pFile, "endmodule\n" ); @@ -1351,7 +1352,8 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName ) fprintf( pFile, "module LUT6 #( parameter INIT = 64\'h0 ) ( output O, input I0, I1, I2, I3, I4, I5 );\n" ); fprintf( pFile, " assign O = INIT[ {I5, I4, I3, I2, I1, I0} ];\n" ); - fprintf( pFile, "endmodule\n\n" ); + fprintf( pFile, "endmodule\n" ); + fprintf( pFile, "`endif\n\n" ); // Write main module fprintf( pFile, "module " ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dbb5ed99e..2071b9d57 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -659,6 +659,7 @@ static int Abc_CommandAbc9MulFind3 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9BsFind ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AndCare ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cuts ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Divide ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1506,8 +1507,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mulfind3", Abc_CommandAbc9MulFind3, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bsfind", Abc_CommandAbc9BsFind, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&andcare", Abc_CommandAbc9AndCare, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&cuts", Abc_CommandAbc9Cuts, 0 ); - + Cmd_CommandAdd( pAbc, "ABC9", "&cuts", Abc_CommandAbc9Cuts, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "÷", Abc_CommandAbc9Divide, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 ); @@ -34455,9 +34457,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) Aig_Man_t * pAig; Gia_Man_t * pGia, * pTemp; char * pInits; - int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fVerbose = 0; + int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fReuseNames = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cmnvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cmnrvh" ) ) != EOF ) { switch ( c ) { @@ -34470,6 +34472,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'n': fNames ^= 1; break; + case 'r': + fReuseNames ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -34532,17 +34537,38 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) pGia->vOutReqs = Vec_FltAllocArray( Abc_NtkGetCoRequiredFloats(pNtk), Abc_NtkCoNum(pNtk) ); pGia->And2Delay = pNtk->AndGateDelay; } + if ( fReuseNames ) + { + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "There is no current AIG to reuse names from.\n" ); + return 1; + } + if ( Gia_ManCiNum(pGia) != Gia_ManCiNum(pAbc->pGia) ) + { + Abc_Print( -1, "The number of CIs differ.\n" ); + return 1; + } + if ( Gia_ManCoNum(pGia) != Gia_ManCoNum(pAbc->pGia) ) + { + Abc_Print( -1, "The number of COs differ.\n" ); + return 1; + } + ABC_SWAP( Vec_Ptr_t *, pGia->vNamesIn, pAbc->pGia->vNamesIn ); + ABC_SWAP( Vec_Ptr_t *, pGia->vNamesOut, pAbc->pGia->vNamesOut ); + } Abc_FrameUpdateGia( pAbc, pGia ); return 0; usage: - Abc_Print( -2, "usage: &get [-cmnvh] \n" ); + Abc_Print( -2, "usage: &get [-cmnrvh] \n" ); Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" ); Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" ); Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" ); Abc_Print( -2, "\t-c : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" ); Abc_Print( -2, "\t-m : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" ); Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" ); + Abc_Print( -2, "\t-r : toggles reusing CI/CO names of the current AIG [default = %s]\n", fReuseNames? "yes": "no" ); Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the file name\n"); @@ -42580,6 +42606,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu FILE * pFile; Gia_Man_t * pGia; char * pTemp; + char * pOrigFileName = NULL; int fVerilog, fSystemVerilog; *pAbc_ReadAigerOrVerilogFileStatus = 0; @@ -42607,6 +42634,8 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu { char pCommand[2000]; int RetValue; + // Save the original filename before changing it + pOrigFileName = pFileName; snprintf( pCommand, sizeof(pCommand), "yosys -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"", fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" ); @@ -42625,7 +42654,18 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); if ( pGia == NULL ) + { Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName ); + return NULL; + } + + // If we read from a Verilog file, keep the original filename as the spec + if ( pOrigFileName != NULL ) + { + ABC_FREE( pGia->pSpec ); + pGia->pSpec = Abc_UtilStrsav( pOrigFileName ); + } + return pGia; } @@ -59447,7 +59487,7 @@ int Abc_CommandAbc9Cuts( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: cuts [-KC num] [-tdbvh]\n" ); + Abc_Print( -2, "usage: &cuts [-KC num] [-tdbvh]\n" ); Abc_Print( -2, "\t computes K-input cuts for the nodes in the current AIG\n" ); Abc_Print( -2, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", 2, 14, nCutSize ); Abc_Print( -2, "\t-C num : max number of cuts at a node (%d <= num <= %d) [default = %d]\n", 2, 256, nCutNum ); @@ -59458,6 +59498,76 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Divide( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel ); + int nParts = 2; + int nCutLevel = 0; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "PLvh" ) ) != EOF ) + { + switch ( c ) + { + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nParts = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nParts < 2 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nCutLevel = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCutLevel < 0 ) + goto usage; + break; + case 'v': + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Divide(): There is no AIG.\n" ); + return 0; + } + Gia_ManDupSplit( pAbc->pGia, nParts, nCutLevel ); + return 0; + +usage: + Abc_Print( -2, "usage: ÷ [-P num] [-L num] [-vh]\n" ); + Abc_Print( -2, "\t divides AIG into N parts at different levels\n" ); + Abc_Print( -2, "\t-P num : number of parts to divide into [default = %d]\n", nParts ); + Abc_Print( -2, "\t-L num : cut level (0 = automatic middle level) [default = %d]\n", nCutLevel ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = no]\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index c4744ebe0..3ec0e929a 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -834,32 +834,51 @@ static void Abc_NtkVerifyPrintWords( Vec_Ptr_t * vWords ) } } -void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, - const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, +void Abc_NtkVerifyPrintCex( const int * pModel, const int * pValues1, const int * pValues2, + const char * const * ppInputNames, int nInputs, const char * const * ppOutputNames, int nOutputs, const char * pNtkName1, const char * pNtkName2 ) { Vec_Ptr_t * vInputs = Vec_PtrAlloc( 0 ); Vec_Ptr_t * vOutputs1 = Vec_PtrAlloc( 0 ); Vec_Ptr_t * vOutputs2 = Vec_PtrAlloc( 0 ); + char * pBaseName1 = NULL; + char * pBaseName2 = NULL; + Abc_NtkVerifyCollectWords( vInputs, ppInputNames, pModel, nInputs ); Abc_NtkVerifyCollectWords( vOutputs1, ppOutputNames, pValues1, nOutputs ); if ( pValues2 ) Abc_NtkVerifyCollectWords( vOutputs2, ppOutputNames, pValues2, nOutputs ); + + // Extract base names for printing + if ( pNtkName1 ) + { + char * pFileNameOnly = Extra_FileNameWithoutPath( (char *)pNtkName1 ); + pBaseName1 = Extra_FileNameGeneric( pFileNameOnly ); + } + if ( pNtkName2 ) + { + char * pFileNameOnly = Extra_FileNameWithoutPath( (char *)pNtkName2 ); + pBaseName2 = Extra_FileNameGeneric( pFileNameOnly ); + } + if ( Vec_PtrSize(vInputs) || Vec_PtrSize(vOutputs1) || Vec_PtrSize(vOutputs2) ) { printf( "INPUT: " ); Abc_NtkVerifyPrintWords( vInputs ); printf( ". OUTPUT: " ); Abc_NtkVerifyPrintWords( vOutputs1 ); - printf( " (%s)", pNtkName1 ? pNtkName1 : "network1" ); + printf( " (%s)", pBaseName1 ? pBaseName1 : (pNtkName1 ? pNtkName1 : "network1") ); if ( pValues2 && Vec_PtrSize(vOutputs2) ) { printf( ", " ); Abc_NtkVerifyPrintWords( vOutputs2 ); - printf( " (%s)", pNtkName2 ? pNtkName2 : "network2" ); + printf( " (%s)", pBaseName2 ? pBaseName2 : (pNtkName2 ? pNtkName2 : "network2") ); } printf( ".\n" ); } + + ABC_FREE( pBaseName1 ); + ABC_FREE( pBaseName2 ); Abc_NtkVerifyFreeWords( vInputs ); Abc_NtkVerifyFreeWords( vOutputs1 ); Abc_NtkVerifyFreeWords( vOutputs2 ); From 6c8b2cfa3b7753d9eba198d3085598aba51b8b16 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Feb 2026 12:19:04 -0800 Subject: [PATCH 07/17] Compiler problem. --- src/aig/gia/giaDup.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ba0b7d78c..d1187cb24 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -6905,7 +6905,7 @@ void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel ) // Create Part 0 (bottom part: levels 0 to Lcut) pPart0 = Gia_ManStart( Gia_ManObjNum(p) ); - pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part0" ); + pFileName = Extra_FileNameGenericAppend( (char *)(p->pSpec ? p->pSpec : "network.aig"), "_part0" ); pPart0->pName = Abc_UtilStrsav( pFileName ); pPart0->pSpec = Abc_UtilStrsav( pFileName ); Gia_ManFillValue( p ); @@ -6925,7 +6925,7 @@ void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel ) } // Write Part 0 - pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part0.aig" ); + pFileName = Extra_FileNameGenericAppend( (char *)(p->pSpec ? p->pSpec : "network.aig"), "_part0.aig" ); Gia_AigerWrite( pPart0, pFileName, 0, 0, 0 ); printf( "Part 0: PI = %d, PO = %d, AND = %d, written to %s\n", Gia_ManCiNum(pPart0), Gia_ManCoNum(pPart0), Gia_ManAndNum(pPart0), pFileName ); @@ -6933,7 +6933,7 @@ void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel ) // Create Part 1 (top part: levels > Lcut) pPart1 = Gia_ManStart( Gia_ManObjNum(p) ); - pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part1" ); + pFileName = Extra_FileNameGenericAppend( (char *)(p->pSpec ? p->pSpec : "network.aig"), "_part1" ); pPart1->pName = Abc_UtilStrsav( pFileName ); pPart1->pSpec = Abc_UtilStrsav( pFileName ); Gia_ManFillValue( p ); @@ -6953,7 +6953,7 @@ void Gia_ManDupSplit( Gia_Man_t * p, int nParts, int nCutLevel ) } // Write Part 1 - pFileName = Extra_FileNameGenericAppend( p->pSpec ? p->pSpec : "network.aig", "_part1.aig" ); + pFileName = Extra_FileNameGenericAppend( (char *)(p->pSpec ? p->pSpec : "network.aig"), "_part1.aig" ); Gia_AigerWrite( pPart1, pFileName, 0, 0, 0 ); printf( "Part 1: PI = %d, PO = %d, AND = %d, written to %s\n", Gia_ManCiNum(pPart1), Gia_ManCoNum(pPart1), Gia_ManAndNum(pPart1), pFileName ); From c7ea67b7df375cae5bbee8fefc1031bc9bf97445 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Feb 2026 12:19:32 -0800 Subject: [PATCH 08/17] Update command "history". --- src/base/cmd/cmd.c | 60 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 50 insertions(+), 10 deletions(-) diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index fff4fa9f6..0bb4b412b 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -441,6 +441,7 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) char * pName, * pStr = NULL; int i, c; int nPrints = 20; + int nPrinted = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { @@ -452,29 +453,68 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) goto usage; } } - if ( argc > globalUtilOptind + 1 ) + if ( argc > globalUtilOptind + 2 ) goto usage; - // get the number from the command line - pStr = argc == globalUtilOptind+1 ? argv[globalUtilOptind] : NULL; - if ( pStr && pStr[0] >= '1' && pStr[0] <= '9' ) - nPrints = atoi(pStr), pStr = NULL; + // parse arguments: can be [substring] [number] in either order + if ( argc == globalUtilOptind + 1 ) + { + // one argument: either number or substring + pStr = argv[globalUtilOptind]; + if ( pStr && pStr[0] >= '1' && pStr[0] <= '9' ) + { + nPrints = atoi(pStr); + pStr = NULL; + } + } + else if ( argc == globalUtilOptind + 2 ) + { + // two arguments: substring and number + char * arg1 = argv[globalUtilOptind]; + char * arg2 = argv[globalUtilOptind + 1]; + + // Try to parse second argument as number + if ( arg2[0] >= '1' && arg2[0] <= '9' ) + { + pStr = arg1; + nPrints = atoi(arg2); + } + // Try to parse first argument as number + else if ( arg1[0] >= '1' && arg1[0] <= '9' ) + { + nPrints = atoi(arg1); + pStr = arg2; + } + else + { + // Neither is a number, error + goto usage; + } + } + // print the commands if ( pStr == NULL ) { + // No search string, show last nPrints entries Vec_PtrForEachEntryStart( char *, pAbc->aHistory, pName, i, Abc_MaxInt(0, Vec_PtrSize(pAbc->aHistory)-nPrints) ) - fprintf( pAbc->Out, "%2d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); + fprintf( pAbc->Out, "%4d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); } else { + // Search string provided, show up to nPrints matching entries Vec_PtrForEachEntry( char *, pAbc->aHistory, pName, i ) if ( strstr(pName, pStr) ) - fprintf( pAbc->Out, "%2d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); + { + fprintf( pAbc->Out, "%4d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); + if ( ++nPrinted >= nPrints ) + break; + } } return 0; usage: - fprintf( pAbc->Err, "usage: history [-h] \n" ); + fprintf( pAbc->Err, "usage: history [-h] [substring] [num]\n" ); fprintf( pAbc->Err, "\t lists the last commands entered on the command line\n" ); - fprintf( pAbc->Err, "\t-h : print the command usage\n" ); - fprintf( pAbc->Err, "\t : the maximum number of entries to show [default = %d]\n", nPrints ); + fprintf( pAbc->Err, "\t-h : print the command usage\n" ); + fprintf( pAbc->Err, "\tsubstring : search for commands containing this substring\n" ); + fprintf( pAbc->Err, "\tnum : the maximum number of entries to show [default = %d]\n", nPrints ); return ( 1 ); } From 71c24a48124a8244a8bb9afed163f678c6a2e325 Mon Sep 17 00:00:00 2001 From: Jonathan Greene Date: Thu, 19 Feb 2026 13:24:41 -0800 Subject: [PATCH 09/17] Fix backward required-time propagation through boxes --- src/aig/gia/giaSpeedup.c | 26 ++++++++++++++++++++++++++ src/misc/tim/timTime.c | 2 +- 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index 0c9d75098..0786bd559 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -333,6 +333,32 @@ float Gia_ManDelayTraceLut( Gia_Man_t * p ) Gia_ObjSetTimeArrival( p, i, tArrival ); } + // update levels of box output CIs to reflect box structure + // (Gia_ManLevelNum assigns level 0 to all CIs, but box output CIs + // need higher levels so that Gia_ManOrderReverse processes them + // before box input COs during the backward required-time pass) + if ( p->pManTime ) + { + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + int iBox, nBoxes = Tim_ManBoxNum( pManTime ); + for ( iBox = 0; iBox < nBoxes; iBox++ ) + { + int nIns = Tim_ManBoxInputNum( pManTime, iBox ); + int nOuts = Tim_ManBoxOutputNum( pManTime, iBox ); + int iCoFirst = Tim_ManBoxInputFirst( pManTime, iBox ); + int iCiFirst = Tim_ManBoxOutputFirst( pManTime, iBox ); + int j, maxLevel = 0; + for ( j = 0; j < nIns; j++ ) + { + int coLevel = Gia_ObjLevel( p, Gia_ManCo(p, iCoFirst + j) ); + if ( coLevel > maxLevel ) + maxLevel = coLevel; + } + for ( j = 0; j < nOuts; j++ ) + Gia_ObjSetLevel( p, Gia_ManCi(p, iCiFirst + j), maxLevel + 1 ); + } + } + // get the latest arrival times tArrival = -TIM_ETERNITY; Gia_ManForEachCo( p, pObj, i ) diff --git a/src/misc/tim/timTime.c b/src/misc/tim/timTime.c index c766fb7f1..578eead31 100644 --- a/src/misc/tim/timTime.c +++ b/src/misc/tim/timTime.c @@ -249,7 +249,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) Tim_ManBoxForEachOutput( p, pBox, pObj, k ) { pDelays = pTable + 3 + k * pBox->nInputs; - if ( pDelays[k] != -ABC_INFINITY ) + if ( pDelays[i] != -ABC_INFINITY ) DelayBest = Abc_MinFloat( DelayBest, pObj->timeReq - pDelays[i] ); } pObjRes->timeReq = DelayBest; From 771e70381c7ea41c81067f59ce653f8756830af0 Mon Sep 17 00:00:00 2001 From: Jonathan Greene Date: Fri, 20 Feb 2026 11:43:09 -0800 Subject: [PATCH 10/17] Fix two bugs causing problems with &trace and boxes. --- src/aig/gia/giaAiger.c | 15 +++++++++++++++ src/aig/gia/giaSpeedup.c | 2 +- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index e9e9e67ca..39fed2fd4 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -677,6 +677,14 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi } pNew->vOutReqs = Vec_FltStart( nOutputs ); memcpy( Vec_FltArray(pNew->vOutReqs), pCur, (size_t)4*nOutputs ); pCur += 4*nOutputs; + // Convert -1.0 back to TIM_ETERNITY for internal use + { + float * pArr = Vec_FltArray(pNew->vOutReqs); + int i; + for ( i = 0; i < nOutputs; i++ ) + if ( pArr[i] < 0 ) + pArr[i] = TIM_ETERNITY; + } if ( fVerbose ) printf( "Finished reading extension \"o\".\n" ); } // read equivalence classes @@ -1562,6 +1570,13 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in { int nPos = Tim_ManPoNum((Tim_Man_t *)p->pManTime); int nFlops = Gia_ManRegNum(p); + // Convert TIM_ETERNITY sentinel to -1.0 per XAIG spec + { + int i; + for ( i = 0; i < nPos + nFlops; i++ ) + if ( pTimes[i] >= TIM_ETERNITY ) + pTimes[i] = -1.0; + } fprintf( pFile, "o" ); Gia_FileWriteBufferSize( pFile, 4*(nPos + nFlops) ); fwrite( pTimes, 1, 4*(nPos + nFlops), pFile ); diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index 0786bd559..aa39c9bcd 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -350,7 +350,7 @@ float Gia_ManDelayTraceLut( Gia_Man_t * p ) int j, maxLevel = 0; for ( j = 0; j < nIns; j++ ) { - int coLevel = Gia_ObjLevel( p, Gia_ManCo(p, iCoFirst + j) ); + int coLevel = Gia_ObjLevel( p, Gia_ObjFanin0(Gia_ManCo(p, iCoFirst + j)) ); if ( coLevel > maxLevel ) maxLevel = coLevel; } From 3b5036a1e1175a05c307b50393c2f1667490fd5a Mon Sep 17 00:00:00 2001 From: Jonathan Greene Date: Sat, 21 Feb 2026 16:54:27 -0800 Subject: [PATCH 11/17] Fix required time handling for unconstrained POs, infinity arithmetic, and absDup cosmetic - Tim_ManInitPoRequiredAll: only overwrite PO required times when ALL are unconstrained; preserve user-specified constraints - Gia_ObjPropagateRequired: propagate infinity unchanged through LUTs - Tim_ManGetCoRequired: guard against infinity minus delay arithmetic - Gia_ManDelayTraceLut: handle infinite required times in slack computation; allow negative slack to report timing violations - Tim_ManCreate: fix required-time loading to address actual POs via Tim_ManForEachPo instead of p->pCos[] (wrong for designs with boxes) - Tim_ManGetArrTimes/Tim_ManGetReqTimes: fix loop-exit detection using boolean flag instead of comparing iterator index against PO/PI count - Gia_ManPrintFlopClasses: use Gia_ManRegBoxNum instead of Gia_ManRegNum Co-Authored-By: Claude Opus 4.6 --- src/aig/gia/giaSpeedup.c | 11 ++++++++--- src/misc/tim/timMan.c | 41 +++++++++++++++++++++++++--------------- src/misc/tim/timTime.c | 7 ++++++- src/proof/abs/absDup.c | 4 ++-- 4 files changed, 42 insertions(+), 21 deletions(-) diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index aa39c9bcd..4212c8966 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -209,6 +209,9 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting ) float tRequired = 0.0; // Suppress "might be used uninitialized" float * pDelays; assert( Gia_ObjIsLut(p, iObj) ); + // Infinity propagates unchanged + if ( Gia_ObjTimeRequired( p, iObj ) >= TIM_ETERNITY ) + return TIM_ETERNITY; if ( pLutLib == NULL && pCellLib == NULL ) { tRequired = Gia_ObjTimeRequired( p, iObj) - (float)1.0; @@ -407,9 +410,11 @@ float Gia_ManDelayTraceLut( Gia_Man_t * p ) } // set slack for this object - tSlack = Gia_ObjTimeRequired(p, iObj) - Gia_ObjTimeArrival(p, iObj); - assert( tSlack + 0.01 > 0.0 ); - Gia_ObjSetTimeSlack( p, iObj, tSlack < 0.0 ? 0.0 : tSlack ); + if ( Gia_ObjTimeRequired(p, iObj) >= TIM_ETERNITY ) + tSlack = TIM_ETERNITY; + else + tSlack = Gia_ObjTimeRequired(p, iObj) - Gia_ObjTimeArrival(p, iObj); + Gia_ObjSetTimeSlack( p, iObj, tSlack ); } Vec_IntFree( vObjs ); return tArrival; diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 274dc0c0e..59eac5a0d 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -591,19 +591,16 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * { // Handle special case when timing is only for POs (without boxes/flops) // This happens when old files provide timing for actual design POs only - if ( Vec_FltSize(vOutReqs) < Tim_ManPoNum(p) ) + if ( Vec_FltSize(vOutReqs) <= Tim_ManPoNum(p) ) { - // Special case: timing for actual POs only (less than Tim_ManPoNum when boxes exist) - for ( i = 0; i < Vec_FltSize(vOutReqs); i++ ) - p->pCos[i].timeReq = Vec_FltEntry(vOutReqs, i); - } - else if ( Vec_FltSize(vOutReqs) == Tim_ManPoNum(p) ) - { - // Original case: timing for POs + // Timing for POs (may be partial — omitted entries stay at TIM_ETERNITY) k = 0; Tim_ManForEachPo( p, pObj, i ) + { + if ( k >= Vec_FltSize(vOutReqs) ) + break; pObj->timeReq = Vec_FltEntry(vOutReqs, k++); - assert( k == Tim_ManPoNum(p) ); + } } else { @@ -633,20 +630,27 @@ float * Tim_ManGetArrTimes( Tim_Man_t * p, int nRegs ) float * pTimes; Tim_Obj_t * pObj; int i; + int fFoundTiming = 0; // Check if any PIs have non-zero arrival times Tim_ManForEachPi( p, pObj, i ) if ( pObj->timeArr != 0.0 ) + { + fFoundTiming = 1; break; - if ( i == Tim_ManPiNum(p) && nRegs > 0 ) + } + if ( !fFoundTiming && nRegs > 0 ) { // Check if any flops have non-zero arrival times for ( i = Tim_ManCiNum(p) - nRegs; i < Tim_ManCiNum(p); i++ ) if ( p->pCis[i].timeArr != 0.0 ) + { + fFoundTiming = 1; break; - if ( i == Tim_ManCiNum(p) ) + } + if ( !fFoundTiming ) return NULL; // No timing info at all } - else if ( i == Tim_ManPiNum(p) ) + else if ( !fFoundTiming ) return NULL; // Allocate array for PIs + Flops (compact format, no box outputs) pTimes = ABC_FALLOC( float, Tim_ManPiNum(p) + nRegs ); @@ -663,20 +667,27 @@ float * Tim_ManGetReqTimes( Tim_Man_t * p, int nRegs ) float * pTimes; Tim_Obj_t * pObj; int i, k = 0; + int fFoundConstraint = 0; // Check if any POs have non-infinity required times Tim_ManForEachPo( p, pObj, i ) if ( pObj->timeReq != TIM_ETERNITY ) + { + fFoundConstraint = 1; break; - if ( i == Tim_ManPoNum(p) && nRegs > 0 ) + } + if ( !fFoundConstraint && nRegs > 0 ) { // Check if any flops have non-infinity required times for ( i = Tim_ManCoNum(p) - nRegs; i < Tim_ManCoNum(p); i++ ) if ( p->pCos[i].timeReq != TIM_ETERNITY ) + { + fFoundConstraint = 1; break; - if ( i == Tim_ManCoNum(p) ) + } + if ( !fFoundConstraint ) return NULL; // No timing info at all } - else if ( i == Tim_ManPoNum(p) ) + else if ( !fFoundConstraint ) return NULL; // Allocate array for POs + Flops (compact format, no box inputs) pTimes = ABC_FALLOC( float, Tim_ManPoNum(p) + nRegs ); diff --git a/src/misc/tim/timTime.c b/src/misc/tim/timTime.c index 578eead31..cc0aa5ffd 100644 --- a/src/misc/tim/timTime.c +++ b/src/misc/tim/timTime.c @@ -98,6 +98,11 @@ void Tim_ManInitPoRequiredAll( Tim_Man_t * p, float Delay ) { Tim_Obj_t * pObj; int i; + // If any PO or flop-input CO is constrained, leave all unchanged + Tim_ManForEachPo( p, pObj, i ) + if ( pObj->timeReq < TIM_ETERNITY ) + return; + // All unconstrained — set to max arrival time Tim_ManForEachPo( p, pObj, i ) Tim_ManSetCoRequired( p, i, Delay ); } @@ -249,7 +254,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) Tim_ManBoxForEachOutput( p, pBox, pObj, k ) { pDelays = pTable + 3 + k * pBox->nInputs; - if ( pDelays[i] != -ABC_INFINITY ) + if ( pDelays[i] != -ABC_INFINITY && pObj->timeReq < TIM_ETERNITY ) DelayBest = Abc_MinFloat( DelayBest, pObj->timeReq - pDelays[i] ); } pObjRes->timeReq = DelayBest; diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c index 942155753..8bd3b537a 100644 --- a/src/proof/abs/absDup.c +++ b/src/proof/abs/absDup.c @@ -303,7 +303,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) int Counter0, Counter1; if ( p->vFlopClasses == NULL ) return; - if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) ) + if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegBoxNum(p) ) { printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" ); return; @@ -312,7 +312,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ", Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) ); - if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) + if ( Counter0 + Counter1 < Gia_ManRegBoxNum(p) ) printf( "and there are other FF classes..." ); printf( "\n" ); } From ec8b45add3752be2e870c80983acafb79eddfcbc Mon Sep 17 00:00:00 2001 From: JingrenWang Date: Mon, 23 Feb 2026 15:42:58 +0800 Subject: [PATCH 12/17] Fix(Windows): Update to windows-2025 Signed-off-by: JingrenWang --- .github/workflows/build-windows.yml | 204 ++++++++++++++++++++++++---- 1 file changed, 178 insertions(+), 26 deletions(-) diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index c9f5e2b4f..6ed4a74b4 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -8,7 +8,7 @@ jobs: build-windows: - runs-on: windows-2019 + runs-on: windows-2025 steps: @@ -17,36 +17,188 @@ jobs: with: submodules: recursive - - name: Prepare MSVC - uses: bus1/cabuild/action/msdevshell@v1 + - name: Setup MSVC + uses: ilammy/msvc-dev-cmd@v1 with: - architecture: x86 + arch: x86 - - name: Upgrade project files to latest Visual Studio, ignoring upgrade errors, and build + - name: Generate solution and project files from dsp + shell: powershell run: | - devenv abcspace.dsw /upgrade - # Fix the upgraded vcxproj files to use C++17 - if (Test-Path abclib.vcxproj) { - $content = Get-Content abclib.vcxproj -Raw - if ($content -match '') { - $content = $content -replace 'Default', 'stdcpp17' - } else { - # Add LanguageStandard if it doesn't exist - $content = $content -replace '()', '$1stdcpp17' + # Parse source files from abclib.dsp + $dspContent = Get-Content "abclib.dsp" -Raw + # Match SOURCE=. followed by path (e.g., SOURCE=.\src\base\abc\abc.c) + # Capture the path without the leading backslash + $sourceFiles = [regex]::Matches($dspContent, 'SOURCE=\.\\([^\r\n]+)') | ForEach-Object { $_.Groups[1].Value } | Sort-Object -Unique + + Write-Host "Found $($sourceFiles.Count) source files" + + # Create the solution file (use tabs for indentation) + $slnContent = "Microsoft Visual Studio Solution File, Format Version 12.00`r`n" + $slnContent += "VisualStudioVersion = 17.0.31903.59`r`n" + $slnContent += "MinimumVisualStudioVersion = 10.0.40219.1`r`n" + $slnContent += 'Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "abclib", "abclib.vcxproj", "{6B6D7E0F-1234-4567-89AB-CDEF01234567}"' + "`r`n" + $slnContent += "EndProject`r`n" + $slnContent += 'Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "abcexe", "abcexe.vcxproj", "{6B6D7E0F-1234-4567-89AB-CDEF01234568}"' + "`r`n" + $slnContent += "`tProjectSection(ProjectDependencies) = postProject`r`n" + $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234567} = {6B6D7E0F-1234-4567-89AB-CDEF01234567}`r`n" + $slnContent += "`tEndProjectSection`r`n" + $slnContent += "EndProject`r`n" + $slnContent += "Global`r`n" + $slnContent += "`tGlobalSection(SolutionConfigurationPlatforms) = preSolution`r`n" + $slnContent += "`t`tRelease|Win32 = Release|Win32`r`n" + $slnContent += "`tEndGlobalSection`r`n" + $slnContent += "`tGlobalSection(ProjectConfigurationPlatforms) = postSolution`r`n" + $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234567}.Release|Win32.ActiveCfg = Release|Win32`r`n" + $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234567}.Release|Win32.Build.0 = Release|Win32`r`n" + $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234568}.Release|Win32.ActiveCfg = Release|Win32`r`n" + $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234568}.Release|Win32.Build.0 = Release|Win32`r`n" + $slnContent += "`tEndGlobalSection`r`n" + $slnContent += "EndGlobal`r`n" + Set-Content "abcspace.sln" $slnContent -NoNewline + + # Build source file items for vcxproj + # Separate .c and .cpp files - .c files compile as C, .cpp files compile as C++ + $cCompileItems = "" + $cppCompileItems = "" + $clIncludeItems = "" + foreach ($src in $sourceFiles) { + if ($src -match '\.c$') { + $cCompileItems += " `r`n" + } elseif ($src -match '\.(cpp|cc)$') { + $cppCompileItems += " `r`n" + } elseif ($src -match '\.h$') { + $clIncludeItems += " `r`n" } - Set-Content abclib.vcxproj -NoNewline $content } - if (Test-Path abcexe.vcxproj) { - $content = Get-Content abcexe.vcxproj -Raw - if ($content -match '') { - $content = $content -replace 'Default', 'stdcpp17' - } else { - # Add LanguageStandard if it doesn't exist - $content = $content -replace '()', '$1stdcpp17' - } - Set-Content abcexe.vcxproj -NoNewline $content - } - msbuild abcspace.sln /m /nologo /v:m /p:Configuration=Release /p:UseMultiToolTask=true /p:PlatformToolset=v142 /p:PreprocessorDefinitions="_WINSOCKAPI_" + + # Create abclib.vcxproj (static library) + $libVcxproj = '' + "`r`n" + $libVcxproj += '' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' Release' + "`r`n" + $libVcxproj += ' Win32' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' 17.0' + "`r`n" + $libVcxproj += ' {6B6D7E0F-1234-4567-89AB-CDEF01234567}' + "`r`n" + $libVcxproj += ' Win32Proj' + "`r`n" + $libVcxproj += ' abclib' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' StaticLibrary' + "`r`n" + $libVcxproj += ' false' + "`r`n" + $libVcxproj += ' v143' + "`r`n" + $libVcxproj += ' true' + "`r`n" + $libVcxproj += ' MultiByte' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' lib\' + "`r`n" + $libVcxproj += ' ReleaseLib\' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' Level3' + "`r`n" + $libVcxproj += ' 4146;4334;4996;4703;%(DisableSpecificWarnings)' + "`r`n" + $libVcxproj += ' true' + "`r`n" + $libVcxproj += ' true' + "`r`n" + $libVcxproj += ' true' + "`r`n" + $libVcxproj += ' WIN32;WINDOWS;NDEBUG;_LIB;ABC_DLL=ABC_DLLEXPORT;_CRT_SECURE_NO_DEPRECATE;_CRT_NONSTDC_NO_WARNINGS;ABC_USE_PTHREADS;ABC_USE_CUDD;HAVE_STRUCT_TIMESPEC;_WINSOCKAPI_;%(PreprocessorDefinitions)' + "`r`n" + $libVcxproj += ' true' + "`r`n" + $libVcxproj += ' stdcpp17' + "`r`n" + $libVcxproj += ' src' + "`r`n" + $libVcxproj += ' /Zc:strictStrings- %(AdditionalOptions)' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' $(OutDir)abcr.lib' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += $cCompileItems + $libVcxproj += $cppCompileItems + $libVcxproj += $clIncludeItems + $libVcxproj += ' ' + "`r`n" + $libVcxproj += ' ' + "`r`n" + $libVcxproj += '' + "`r`n" + Set-Content "abclib.vcxproj" $libVcxproj -NoNewline + + # Create abcexe.vcxproj (executable) + $exeVcxproj = '' + "`r`n" + $exeVcxproj += '' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' Release' + "`r`n" + $exeVcxproj += ' Win32' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' 17.0' + "`r`n" + $exeVcxproj += ' {6B6D7E0F-1234-4567-89AB-CDEF01234568}' + "`r`n" + $exeVcxproj += ' Win32Proj' + "`r`n" + $exeVcxproj += ' abcexe' + "`r`n" + $exeVcxproj += ' abc' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' Application' + "`r`n" + $exeVcxproj += ' false' + "`r`n" + $exeVcxproj += ' v143' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' MultiByte' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' _TEST\' + "`r`n" + $exeVcxproj += ' ReleaseExe\' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' Level3' + "`r`n" + $exeVcxproj += ' 4146;4334;4996;4703;%(DisableSpecificWarnings)' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' WIN32;WINDOWS;NDEBUG;_CONSOLE;ABC_DLL=ABC_DLLEXPORT;_CRT_SECURE_NO_DEPRECATE;_CRT_NONSTDC_NO_WARNINGS;ABC_USE_PTHREADS;ABC_USE_CUDD;HAVE_STRUCT_TIMESPEC;_WINSOCKAPI_;%(PreprocessorDefinitions)' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' stdcpp17' + "`r`n" + $exeVcxproj += ' src' + "`r`n" + $exeVcxproj += ' /Zc:strictStrings- %(AdditionalOptions)' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' Console' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' true' + "`r`n" + $exeVcxproj += ' kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;lib\x86\pthreadVC2.lib;%(AdditionalDependencies)' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' {6B6D7E0F-1234-4567-89AB-CDEF01234567}' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += ' ' + "`r`n" + $exeVcxproj += '' + "`r`n" + Set-Content "abcexe.vcxproj" $exeVcxproj -NoNewline + + Write-Host "Project files generated successfully" + + - name: Build + run: | + msbuild abcspace.sln /m /nologo /v:m /p:Configuration=Release /p:Platform=Win32 /p:UseMultiToolTask=true if ($LASTEXITCODE -ne 0) { throw "Build failed with exit code $LASTEXITCODE" } - name: Test Executable From ce559b169e6b0efc61741902e3f9e4f5ef3fff6f Mon Sep 17 00:00:00 2001 From: JingrenWang Date: Tue, 24 Feb 2026 08:37:49 +0800 Subject: [PATCH 13/17] Refactor(Workflow): Windows build refactor Signed-off-by: JingrenWang --- .github/scripts/abcexe.vcxproj | 62 +++++++++ .github/scripts/abclib.vcxproj.template | 52 +++++++ .github/scripts/abcspace.sln | 22 +++ .github/workflows/build-windows.yml | 175 +++--------------------- .gitignore | 4 +- 5 files changed, 155 insertions(+), 160 deletions(-) create mode 100644 .github/scripts/abcexe.vcxproj create mode 100644 .github/scripts/abclib.vcxproj.template create mode 100644 .github/scripts/abcspace.sln diff --git a/.github/scripts/abcexe.vcxproj b/.github/scripts/abcexe.vcxproj new file mode 100644 index 000000000..817e0809e --- /dev/null +++ b/.github/scripts/abcexe.vcxproj @@ -0,0 +1,62 @@ + + + + + Release + Win32 + + + + 17.0 + {6B6D7E0F-1234-4567-89AB-CDEF01234568} + Win32Proj + abcexe + abc + + + + Application + false + v143 + true + MultiByte + + + + + + + _TEST\ + ReleaseExe\ + + + + Level3 + 4146;4334;4996;4703;%(DisableSpecificWarnings) + true + true + true + WIN32;WINDOWS;NDEBUG;_CONSOLE;ABC_DLL=ABC_DLLEXPORT;_CRT_SECURE_NO_DEPRECATE;_CRT_NONSTDC_NO_WARNINGS;ABC_USE_PTHREADS;ABC_USE_CUDD;HAVE_STRUCT_TIMESPEC;_WINSOCKAPI_;%(PreprocessorDefinitions) + true + stdcpp17 + src + /Zc:strictStrings- %(AdditionalOptions) + + + Console + true + true + true + kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;lib\x86\pthreadVC2.lib;%(AdditionalDependencies) + + + + + + + + {6B6D7E0F-1234-4567-89AB-CDEF01234567} + + + + diff --git a/.github/scripts/abclib.vcxproj.template b/.github/scripts/abclib.vcxproj.template new file mode 100644 index 000000000..77498528d --- /dev/null +++ b/.github/scripts/abclib.vcxproj.template @@ -0,0 +1,52 @@ + + + + + Release + Win32 + + + + 17.0 + {6B6D7E0F-1234-4567-89AB-CDEF01234567} + Win32Proj + abclib + + + + StaticLibrary + false + v143 + true + MultiByte + + + + + + + lib\ + ReleaseLib\ + + + + Level3 + 4146;4334;4996;4703;%(DisableSpecificWarnings) + true + true + true + WIN32;WINDOWS;NDEBUG;_LIB;ABC_DLL=ABC_DLLEXPORT;_CRT_SECURE_NO_DEPRECATE;_CRT_NONSTDC_NO_WARNINGS;ABC_USE_PTHREADS;ABC_USE_CUDD;HAVE_STRUCT_TIMESPEC;_WINSOCKAPI_;%(PreprocessorDefinitions) + true + stdcpp17 + src + /Zc:strictStrings- %(AdditionalOptions) + + + $(OutDir)abcr.lib + + + +{{SOURCE_FILES}} + + + diff --git a/.github/scripts/abcspace.sln b/.github/scripts/abcspace.sln new file mode 100644 index 000000000..2c6890579 --- /dev/null +++ b/.github/scripts/abcspace.sln @@ -0,0 +1,22 @@ +Microsoft Visual Studio Solution File, Format Version 12.00 +# Visual Studio Version 17 +VisualStudioVersion = 17.0.31903.59 +MinimumVisualStudioVersion = 10.0.40219.1 +Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "abclib", "abclib.vcxproj", "{6B6D7E0F-1234-4567-89AB-CDEF01234567}" +EndProject +Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "abcexe", "abcexe.vcxproj", "{6B6D7E0F-1234-4567-89AB-CDEF01234568}" + ProjectSection(ProjectDependencies) = postProject + {6B6D7E0F-1234-4567-89AB-CDEF01234567} = {6B6D7E0F-1234-4567-89AB-CDEF01234567} + EndProjectSection +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + Release|Win32 = Release|Win32 + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {6B6D7E0F-1234-4567-89AB-CDEF01234567}.Release|Win32.ActiveCfg = Release|Win32 + {6B6D7E0F-1234-4567-89AB-CDEF01234567}.Release|Win32.Build.0 = Release|Win32 + {6B6D7E0F-1234-4567-89AB-CDEF01234568}.Release|Win32.ActiveCfg = Release|Win32 + {6B6D7E0F-1234-4567-89AB-CDEF01234568}.Release|Win32.Build.0 = Release|Win32 + EndGlobalSection +EndGlobal diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index 6ed4a74b4..7b6e61304 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -22,179 +22,38 @@ jobs: with: arch: x86 - - name: Generate solution and project files from dsp + - name: Copy project files from scripts + run: | + copy .github\scripts\abcspace.sln . + copy .github\scripts\abcexe.vcxproj . + + - name: Generate abclib.vcxproj from dsp shell: powershell run: | # Parse source files from abclib.dsp $dspContent = Get-Content "abclib.dsp" -Raw - # Match SOURCE=. followed by path (e.g., SOURCE=.\src\base\abc\abc.c) - # Capture the path without the leading backslash $sourceFiles = [regex]::Matches($dspContent, 'SOURCE=\.\\([^\r\n]+)') | ForEach-Object { $_.Groups[1].Value } | Sort-Object -Unique Write-Host "Found $($sourceFiles.Count) source files" - # Create the solution file (use tabs for indentation) - $slnContent = "Microsoft Visual Studio Solution File, Format Version 12.00`r`n" - $slnContent += "VisualStudioVersion = 17.0.31903.59`r`n" - $slnContent += "MinimumVisualStudioVersion = 10.0.40219.1`r`n" - $slnContent += 'Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "abclib", "abclib.vcxproj", "{6B6D7E0F-1234-4567-89AB-CDEF01234567}"' + "`r`n" - $slnContent += "EndProject`r`n" - $slnContent += 'Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "abcexe", "abcexe.vcxproj", "{6B6D7E0F-1234-4567-89AB-CDEF01234568}"' + "`r`n" - $slnContent += "`tProjectSection(ProjectDependencies) = postProject`r`n" - $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234567} = {6B6D7E0F-1234-4567-89AB-CDEF01234567}`r`n" - $slnContent += "`tEndProjectSection`r`n" - $slnContent += "EndProject`r`n" - $slnContent += "Global`r`n" - $slnContent += "`tGlobalSection(SolutionConfigurationPlatforms) = preSolution`r`n" - $slnContent += "`t`tRelease|Win32 = Release|Win32`r`n" - $slnContent += "`tEndGlobalSection`r`n" - $slnContent += "`tGlobalSection(ProjectConfigurationPlatforms) = postSolution`r`n" - $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234567}.Release|Win32.ActiveCfg = Release|Win32`r`n" - $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234567}.Release|Win32.Build.0 = Release|Win32`r`n" - $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234568}.Release|Win32.ActiveCfg = Release|Win32`r`n" - $slnContent += "`t`t{6B6D7E0F-1234-4567-89AB-CDEF01234568}.Release|Win32.Build.0 = Release|Win32`r`n" - $slnContent += "`tEndGlobalSection`r`n" - $slnContent += "EndGlobal`r`n" - Set-Content "abcspace.sln" $slnContent -NoNewline - - # Build source file items for vcxproj - # Separate .c and .cpp files - .c files compile as C, .cpp files compile as C++ - $cCompileItems = "" - $cppCompileItems = "" - $clIncludeItems = "" + # Build source file items + $sourceItems = "" foreach ($src in $sourceFiles) { if ($src -match '\.c$') { - $cCompileItems += " `r`n" + $sourceItems += " `r`n" } elseif ($src -match '\.(cpp|cc)$') { - $cppCompileItems += " `r`n" + $sourceItems += " `r`n" } elseif ($src -match '\.h$') { - $clIncludeItems += " `r`n" + $sourceItems += " `r`n" } } - # Create abclib.vcxproj (static library) - $libVcxproj = '' + "`r`n" - $libVcxproj += '' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' Release' + "`r`n" - $libVcxproj += ' Win32' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' 17.0' + "`r`n" - $libVcxproj += ' {6B6D7E0F-1234-4567-89AB-CDEF01234567}' + "`r`n" - $libVcxproj += ' Win32Proj' + "`r`n" - $libVcxproj += ' abclib' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' StaticLibrary' + "`r`n" - $libVcxproj += ' false' + "`r`n" - $libVcxproj += ' v143' + "`r`n" - $libVcxproj += ' true' + "`r`n" - $libVcxproj += ' MultiByte' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' lib\' + "`r`n" - $libVcxproj += ' ReleaseLib\' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' Level3' + "`r`n" - $libVcxproj += ' 4146;4334;4996;4703;%(DisableSpecificWarnings)' + "`r`n" - $libVcxproj += ' true' + "`r`n" - $libVcxproj += ' true' + "`r`n" - $libVcxproj += ' true' + "`r`n" - $libVcxproj += ' WIN32;WINDOWS;NDEBUG;_LIB;ABC_DLL=ABC_DLLEXPORT;_CRT_SECURE_NO_DEPRECATE;_CRT_NONSTDC_NO_WARNINGS;ABC_USE_PTHREADS;ABC_USE_CUDD;HAVE_STRUCT_TIMESPEC;_WINSOCKAPI_;%(PreprocessorDefinitions)' + "`r`n" - $libVcxproj += ' true' + "`r`n" - $libVcxproj += ' stdcpp17' + "`r`n" - $libVcxproj += ' src' + "`r`n" - $libVcxproj += ' /Zc:strictStrings- %(AdditionalOptions)' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' $(OutDir)abcr.lib' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += $cCompileItems - $libVcxproj += $cppCompileItems - $libVcxproj += $clIncludeItems - $libVcxproj += ' ' + "`r`n" - $libVcxproj += ' ' + "`r`n" - $libVcxproj += '' + "`r`n" - Set-Content "abclib.vcxproj" $libVcxproj -NoNewline + # Read template and replace placeholder + $template = Get-Content ".github\scripts\abclib.vcxproj.template" -Raw + $vcxproj = $template -replace '\{\{SOURCE_FILES\}\}', $sourceItems + Set-Content "abclib.vcxproj" $vcxproj -NoNewline - # Create abcexe.vcxproj (executable) - $exeVcxproj = '' + "`r`n" - $exeVcxproj += '' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' Release' + "`r`n" - $exeVcxproj += ' Win32' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' 17.0' + "`r`n" - $exeVcxproj += ' {6B6D7E0F-1234-4567-89AB-CDEF01234568}' + "`r`n" - $exeVcxproj += ' Win32Proj' + "`r`n" - $exeVcxproj += ' abcexe' + "`r`n" - $exeVcxproj += ' abc' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' Application' + "`r`n" - $exeVcxproj += ' false' + "`r`n" - $exeVcxproj += ' v143' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' MultiByte' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' _TEST\' + "`r`n" - $exeVcxproj += ' ReleaseExe\' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' Level3' + "`r`n" - $exeVcxproj += ' 4146;4334;4996;4703;%(DisableSpecificWarnings)' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' WIN32;WINDOWS;NDEBUG;_CONSOLE;ABC_DLL=ABC_DLLEXPORT;_CRT_SECURE_NO_DEPRECATE;_CRT_NONSTDC_NO_WARNINGS;ABC_USE_PTHREADS;ABC_USE_CUDD;HAVE_STRUCT_TIMESPEC;_WINSOCKAPI_;%(PreprocessorDefinitions)' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' stdcpp17' + "`r`n" - $exeVcxproj += ' src' + "`r`n" - $exeVcxproj += ' /Zc:strictStrings- %(AdditionalOptions)' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' Console' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' true' + "`r`n" - $exeVcxproj += ' kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib;lib\x86\pthreadVC2.lib;%(AdditionalDependencies)' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' {6B6D7E0F-1234-4567-89AB-CDEF01234567}' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += ' ' + "`r`n" - $exeVcxproj += '' + "`r`n" - Set-Content "abcexe.vcxproj" $exeVcxproj -NoNewline - - Write-Host "Project files generated successfully" + Write-Host "abclib.vcxproj generated successfully" - name: Build run: | @@ -216,4 +75,4 @@ jobs: uses: actions/upload-artifact@v4 with: name: package-windows - path: staging/ + path: staging/ \ No newline at end of file diff --git a/.gitignore b/.gitignore index bef9a6aa4..7236839d3 100644 --- a/.gitignore +++ b/.gitignore @@ -37,7 +37,7 @@ abcext.dsp abcexe.vcproj* abclib.vcproj* -abcspace.sln +/abcspace.sln abcspace.suo *.pyc @@ -62,4 +62,4 @@ tags /cmake /cscope -abc.history +abc.history \ No newline at end of file From ef54c1daea94cac406e3c4bdbbe2ee20c8105c8e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 24 Feb 2026 14:59:13 -0800 Subject: [PATCH 14/17] Updating interface of &cec. --- src/base/abci/abc.c | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2071b9d57..f1bef5e23 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35189,7 +35189,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // Check if we should write LUT-based Verilog - if ( fUseLuts || (Gia_ManHasMapping(pAbc->pGia) && !fUseGates) ) + if ( fUseLuts ) { if ( !Gia_ManHasMapping(pAbc->pGia) ) { @@ -35232,7 +35232,6 @@ usage: Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the file name\n"); - Abc_Print( -2, "\tNote: When AIG is mapped and -l is not specified, LUT-based output is automatically used.\n"); return 1; } @@ -42601,7 +42600,7 @@ usage: SeeAlso [] ***********************************************************************/ -static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, int * pAbc_ReadAigerOrVerilogFileStatus ) +static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus ) { FILE * pFile; Gia_Man_t * pGia; @@ -42637,7 +42636,8 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu // Save the original filename before changing it pOrigFileName = pFileName; snprintf( pCommand, sizeof(pCommand), - "yosys -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"", + "yosys -qp \"read_verilog %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; aigmap; write_aiger -symbols _temp_.aig\"", + pDefines ? "-D" : "", pDefines ? pDefines : "", fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" ); #if defined(__wasm) RetValue = 1; @@ -42685,12 +42685,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars ); Cec_ParCec_t ParsCec, * pPars = &ParsCec; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; - char ** pArgvNew, * pTopModule = NULL; + char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL; int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0; int Abc_ReadAigerOrVerilogFileStatus = 0; Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTMnmdbasxytvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDnmdbasxytvwh" ) ) != EOF ) { switch ( c ) { @@ -42725,6 +42725,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) pTopModule = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by defines.\n" ); + goto usage; + } + pDefines = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'n': pPars->fNaive ^= 1; break; @@ -42846,7 +42855,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) int n; for ( n = 0; n < 2; n++ ) { - pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, &Abc_ReadAigerOrVerilogFileStatus ); + pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[n] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } @@ -42882,7 +42891,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } FileName = pAbc->pGia->pSpec; } - pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, &Abc_ReadAigerOrVerilogFileStatus ); + pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[1] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } @@ -42994,11 +43003,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-nmdbasxytvwh]\n" ); + Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-nmdbasxytvwh]\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); - Abc_Print( -2, "\t-M str : top module name if Verilog file(s) are used [default = %d]\n", pPars->TimeLimit ); + Abc_Print( -2, "\t-M str : top module name if Verilog file(s) are used [default = \"not used\"]\n" ); + Abc_Print( -2, "\t-D str : defines to be used by Yosys for Verilog files [default = \"not used\"]\n" ); Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); From d5c1f2cfe12f23778ac8adfd964e00da7e580113 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 25 Feb 2026 20:00:28 -0800 Subject: [PATCH 15/17] Adding callbacks to "scorr" and "&scorr". --- src/proof/cec/cecCorr.c | 30 ++++++++++++++++++++++++------ src/proof/ssw/sswConstr.c | 8 ++++++++ src/proof/ssw/sswCore.c | 20 +++++++++++++------- src/proof/ssw/sswDyn.c | 2 ++ src/proof/ssw/sswInt.h | 2 +- src/proof/ssw/sswSweep.c | 8 ++++++++ 6 files changed, 56 insertions(+), 14 deletions(-) diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 8d4c730a1..0496b2e49 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -22,6 +22,13 @@ ABC_NAMESPACE_IMPL_START +static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars ) +{ + if ( pPars == NULL || pPars->pFunc == NULL ) + return 0; + return ((int (*)(void *))pPars->pFunc)( pPars->pData ); +} + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -808,6 +815,8 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr fChanges = 1; for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ ) { + if ( Cec_ParCorShouldStop( pPars ) ) + break; abctime clkBmc = Abc_Clock(); fChanges = 0; pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings ); @@ -836,6 +845,8 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr Vec_StrFree( vStatus ); Gia_ManStop( pSrm ); Vec_IntFree( vOutputs ); + if ( Cec_ParCorShouldStop( pPars ) ) + break; } Cec_ManSimStop( pSim ); } @@ -975,10 +986,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) // check the base case if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); - if ( pPars->pFunc ) + if ( Cec_ParCorShouldStop( pPars ) ) { - ((int (*)(void *))pPars->pFunc)( pPars->pData ); - ((int (*)(void *))pPars->pFunc)( pPars->pData ); + Cec_ManSimStop( pSim ); + return 1; } if ( pPars->nStepsMax == 0 ) { @@ -989,6 +1000,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) // perform refinement of equivalence classes for ( r = 0; r < nIterMax; r++ ) { + if ( Cec_ParCorShouldStop( pPars ) ) + { + Cec_ManSimStop( pSim ); + return 1; + } if ( pPars->nStepsMax == r ) { Cec_ManSimStop( pSim ); @@ -1036,8 +1052,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Vec_StrFree( vStatus ); Vec_IntFree( vOutputs ); //Gia_ManEquivPrintClasses( pAig, 1, 0 ); - if ( pPars->pFunc ) - ((int (*)(void *))pPars->pFunc)( pPars->pData ); + if ( Cec_ParCorShouldStop( pPars ) ) + { + Cec_ManSimStop( pSim ); + return 1; + } // quit if const is no longer there if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) ) { @@ -1448,4 +1467,3 @@ Gia_Man_t * Gia_ManDupStopsTest( Gia_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index a3a7e66f3..d8be282fa 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -512,6 +512,8 @@ clk = Abc_Clock(); p->fRefined = 0; for ( f = 0; f < p->pPars->nFramesK; f++ ) { + if ( Ssw_ManCallbackStop(p) ) + break; // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) @@ -540,10 +542,14 @@ clk = Abc_Clock(); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { + if ( Ssw_ManCallbackStop(p) ) + break; pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); p->fRefined |= Ssw_ManSweepNodeConstr( p, pObj, f, 1 ); } + if ( i < Aig_ManObjNumMax(p->pAig) ) + break; // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) break; @@ -692,6 +698,8 @@ p->timeReduce += Abc_Clock() - clk; pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); Aig_ManForEachObj( p->pAig, pObj, i ) { + if ( Ssw_ManCallbackStop(p) ) + break; if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c index 1307d67c9..9add71284 100644 --- a/src/proof/ssw/sswCore.c +++ b/src/proof/ssw/sswCore.c @@ -238,6 +238,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Aig_Man_t * pAigNew; int RetValue, nIter = -1, nPrev[4] = {0}; abctime clk, clkTotal = Abc_Clock(); + abctime nTimeToStop = p->pPars->TimeLimit > 0 ? clkTotal + (abctime)p->pPars->TimeLimit * CLOCKS_PER_SEC : 0; // get the starting stats p->nLitsBeg = Ssw_ClassesLitNum( p->ppClasses ); p->nNodesBeg = Aig_ManNodeNum(p->pAig); @@ -251,6 +252,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) if ( !p->pPars->fLatchCorr || p->pPars->nFramesK > 1 ) { p->pMSat = Ssw_SatStart( 0 ); + if ( nTimeToStop ) + sat_solver_set_runtime_limit( p->pMSat->pSat, nTimeToStop ); if ( p->pPars->fConstrs ) Ssw_ManSweepBmcConstr( p ); else @@ -276,11 +279,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Aig_ManStop( pSRed ); } */ - if ( p->pPars->pFunc ) - { - ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); - ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); - } + if ( Ssw_ManCallbackStop(p) || Ssw_ManCallbackStop(p) ) + goto finalize; if ( p->pPars->nStepsMax == 0 ) { Abc_Print( 1, "Stopped signal correspondence after BMC.\n" ); @@ -290,6 +290,8 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { + if ( nTimeToStop && Abc_Clock() >= nTimeToStop ) + goto finalize; if ( p->pPars->nStepsMax == nIter ) { Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", nIter ); @@ -306,9 +308,13 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) Abc_Print( 1, "If the miter is SAT, the reduced result is incorrect.\n" ); break; } + if ( Ssw_ManCallbackStop(p) ) + goto finalize; clk = Abc_Clock(); p->pMSat = Ssw_SatStart( 0 ); + if ( nTimeToStop ) + sat_solver_set_runtime_limit( p->pMSat->pSat, nTimeToStop ); if ( p->pPars->fLatchCorrOpt ) { RetValue = Ssw_ManSweepLatch( p ); @@ -379,8 +385,8 @@ clk = Abc_Clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; - if ( p->pPars->pFunc ) - ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ); + if ( Ssw_ManCallbackStop(p) ) + goto finalize; if ( p->pPars->nLimitMax ) { int nCur = Ssw_ClassesCand1Num(p->ppClasses); diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c index 316b2e4d1..a2654ca0b 100644 --- a/src/proof/ssw/sswDyn.c +++ b/src/proof/ssw/sswDyn.c @@ -407,6 +407,8 @@ p->timeReduce += Abc_Clock() - clk; p->iNodeStart = 0; Aig_ManForEachObj( p->pAig, pObj, i ) { + if ( Ssw_ManCallbackStop(p) ) + break; if ( p->iNodeStart == 0 ) p->iNodeStart = i; if ( p->pPars->fVerbose ) diff --git a/src/proof/ssw/sswInt.h b/src/proof/ssw/sswInt.h index 006819237..11f60fdd9 100644 --- a/src/proof/ssw/sswInt.h +++ b/src/proof/ssw/sswInt.h @@ -190,6 +190,7 @@ static inline void Ssw_ObjSetFrame_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int static inline Aig_Obj_t * Ssw_ObjChild0Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Ssw_ObjChild1Fra_( Ssw_Frm_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame_(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; } +static inline int Ssw_ManCallbackStop( Ssw_Man_t * p ) { return (p && p->pPars && p->pPars->pFunc) ? ((int (*)(void *))p->pPars->pFunc)( p->pPars->pData ) : 0; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -299,4 +300,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index 2687e9c1c..ead977af3 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -288,6 +288,8 @@ clk = Abc_Clock(); pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK ); for ( f = 0; f < p->pPars->nFramesK; f++ ) { + if ( Ssw_ManCallbackStop(p) ) + break; // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) @@ -298,12 +300,16 @@ clk = Abc_Clock(); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { + if ( Ssw_ManCallbackStop(p) ) + break; if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL ); pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL ); } + if ( i < Aig_ManObjNumMax(p->pAig) ) + break; // quit if this is the last timeframe if ( f == p->pPars->nFramesK - 1 ) break; @@ -415,6 +421,8 @@ p->timeReduce += Abc_Clock() - clk; vObjPairs = (p->pPars->fEquivDump || p->pPars->fEquivDump2)? Vec_IntAlloc(1000) : NULL; Aig_ManForEachObj( p->pAig, pObj, i ) { + if ( Ssw_ManCallbackStop(p) ) + break; if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) From c1937d12ac9fddb26e59bae6fc38b7a7c14959ee Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 25 Feb 2026 20:00:57 -0800 Subject: [PATCH 16/17] Improvements to &sprove. --- src/proof/cec/cecProve.c | 65 ++++++++++++++++++++++++++++++++-------- 1 file changed, 52 insertions(+), 13 deletions(-) diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 273791fe4..2de1b68b6 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -64,6 +64,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in #define PAR_THR_MAX 8 #define PAR_ENGINE_UFAR 6 +#define PAR_ENGINE_SCORR1 7 +#define PAR_ENGINE_SCORR2 8 struct Par_Share_t_ { volatile int fSolved; @@ -82,7 +84,25 @@ typedef struct Par_ThData_t_ Wlc_Ntk_t * pWlc; Par_Share_t * pShare; } Par_ThData_t; +typedef struct Cec_ScorrStop_t_ +{ + Par_Share_t * pShare; + abctime TimeToStop; +} Cec_ScorrStop_t; static volatile Par_Share_t * g_pUfarShare = NULL; +static inline const char * Cec_SolveEngineName( int iEngine ) +{ + if ( iEngine == 0 ) return "rar"; + if ( iEngine == 1 ) return "bmc"; + if ( iEngine == 2 ) return "pdr"; + if ( iEngine == 3 ) return "bmc-glucose"; + if ( iEngine == 4 ) return "pdr-abs"; + if ( iEngine == 5 ) return "bmcg"; + if ( iEngine == PAR_ENGINE_UFAR ) return "ufar"; + if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new"; + if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old"; + return "unknown"; +} static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst ) { char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec; @@ -108,6 +128,17 @@ static int Cec_SProveStopUfar( int RunId ) (void)RunId; return g_pUfarShare && g_pUfarShare->fSolved != 0; } +static int Cec_ScorrStop( void * pUser ) +{ + Cec_ScorrStop_t * p = (Cec_ScorrStop_t *)pUser; + if ( p == NULL ) + return 0; + if ( p->pShare && p->pShare->fSolved ) + return 1; + if ( p->TimeToStop && Abc_Clock() >= p->TimeToStop ) + return 1; + return 0; +} static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result ) { Par_ThData_t * pThData = (Par_ThData_t *)pUser; @@ -273,12 +304,15 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } return RetValue; } -Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) +Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) { + Cec_ScorrStop_t Stop = { pShare, nTimeOut > 0 ? Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC : 0 }; if ( Gia_ManRegNum(p) == 0 ) return Gia_ManDup( p ); Ssw_Pars_t Pars, * pPars = &Pars; Ssw_ManSetDefaultParams( pPars ); + pPars->pFunc = (void *)Cec_ScorrStop; + pPars->pData = (void *)&Stop; Aig_Man_t * pAig = Gia_ManToAigSimple( p ); Aig_Man_t * pAig2 = Ssw_SignalCorrespondence( pAig, pPars ); Gia_Man_t * pGia2 = Gia_ManFromAigSimple( pAig2 ); @@ -286,8 +320,9 @@ Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p ) Aig_ManStop( pAig ); return pGia2; } -Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) +Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) { + Cec_ScorrStop_t Stop = { pShare, nTimeOut > 0 ? Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC : 0 }; if ( Gia_ManRegNum(p) == 0 ) return Gia_ManDup( p ); Cec_ParCor_t Pars, * pPars = &Pars; @@ -296,6 +331,8 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) pPars->nLevelMax = 100; pPars->fVerbose = 0; pPars->fUseCSat = 1; + pPars->pFunc = (void *)Cec_ScorrStop; + pPars->pData = (void *)&Stop; return Cec_ManLSCorrespondence( p, pPars ); } @@ -376,7 +413,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Par_ThData_t ThData[PAR_THR_MAX]; pthread_t WorkerThread[PAR_THR_MAX]; Par_Share_t Share; - int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -2; + int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -1; memset( &Share, 0, sizeof(Par_Share_t) ); Abc_CexFreeP( &p->pCexComb ); Abc_CexFreeP( &p->pCexSeq ); @@ -391,10 +428,10 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share ); // meanwhile, perform scorr - Gia_Man_t * pScorr = Cec_GiaScorrNew( p ); + Gia_Man_t * pScorr = Cec_GiaScorrNew( p, nTimeOut, &Share ); clkScorr = Abc_Clock() - clkTotal; if ( Gia_ManAndNum(pScorr) == 0 ) - RetValue = 1, RetEngine = -1; + RetValue = 1, RetEngine = PAR_ENGINE_SCORR1; RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) @@ -406,15 +443,15 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in } Cec_GiaInitThreads( ThData, nWorkers, pScorr, nTimeOut2, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - // meanwhile, perform scorr - if ( Gia_ManAndNum(pScorr) < 100000 ) + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); + if ( RetValue == -1 && Gia_ManAndNum(pScorr) < 100000 ) { - Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr ); + // Run this reduction only when round-2 did not decide the problem. + Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr, nTimeOut3, &Share ); clkScorr2 = Abc_Clock() - clkStart; if ( Gia_ManAndNum(pScorr2) == 0 ) - RetValue = 1; - - RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); + RetValue = 1, RetEngine = PAR_ENGINE_SCORR2; + if ( RetValue == -1 ) { if ( !fSilent && fVerbose ) { @@ -440,11 +477,13 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in if ( !fSilent ) { char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p); + if ( RetValue != -1 && RetEngine < 0 ) + RetEngine = PAR_ENGINE_SCORR1; printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" ); if ( RetValue == 0 ) - printf( "SATISFIABLE (solved by %d).", RetEngine ); + printf( "SATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); else if ( RetValue == 1 ) - printf( "UNSATISFIABLE (solved by %d).", RetEngine ); + printf( "UNSATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); else if ( RetValue == -1 ) printf( "UNDECIDED." ); else assert( 0 ); From 4e5c5e62af3c5beda477578e55656c2c721ac5f9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 25 Feb 2026 20:18:28 -0800 Subject: [PATCH 17/17] Compiler problem. --- src/proof/cec/cecProve.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c index 2de1b68b6..017296540 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -306,7 +306,9 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par } Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) { - Cec_ScorrStop_t Stop = { pShare, nTimeOut > 0 ? Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC : 0 }; + Cec_ScorrStop_t Stop; + Stop.pShare = pShare; + Stop.TimeToStop = nTimeOut > 0 ? (abctime)(Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC) : 0; if ( Gia_ManRegNum(p) == 0 ) return Gia_ManDup( p ); Ssw_Pars_t Pars, * pPars = &Pars; @@ -322,7 +324,9 @@ Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) } Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare ) { - Cec_ScorrStop_t Stop = { pShare, nTimeOut > 0 ? Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC : 0 }; + Cec_ScorrStop_t Stop; + Stop.pShare = pShare; + Stop.TimeToStop = nTimeOut > 0 ? (abctime)(Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC) : 0; if ( Gia_ManRegNum(p) == 0 ) return Gia_ManDup( p ); Cec_ParCor_t Pars, * pPars = &Pars;