From ad267aca8a4fd2fa0659b1a913531ee3949c46c2 Mon Sep 17 00:00:00 2001 From: JingrenWang Date: Mon, 19 Jan 2026 08:13:08 +0800 Subject: [PATCH 1/5] Fix(Workflow): Bring windows build back to life Signed-off-by: JingrenWang --- .github/workflows/build-windows.yml | 45 +++++++---- abcexe.dsp | 4 +- abclib.dsp | 117 +++++++++++++++++++++++++++- src/aig/gia/giaLutCas.c | 8 ++ src/misc/extra/extra.h | 2 + src/misc/util/abc_global.h | 2 + src/misc/util/utilAigSim.c | 85 ++++++++++++++++++++ src/misc/util/utilNet.c | 8 ++ src/misc/util/utilPrefix.cpp | 1 + src/misc/util/utilPth.c | 32 ++++++++ src/misc/util/winsock_compat.h | 22 ++++++ src/opt/ufar/UfarCmd.cpp | 6 ++ src/opt/ufar/UfarMgr.cpp | 4 + src/opt/ufar/UfarMgr.h | 15 ++++ src/opt/ufar/UfarPth.cpp | 4 + src/opt/untk/NtkNtk.cpp | 4 + src/opt/util/util.cpp | 4 + src/opt/util/util.h | 30 +++++++ src/proof/ssw/sswPart.c | 29 +++++++ src/sat/bmc/bmcMaj.c | 8 ++ src/sat/bmc/bmcMaj8.c | 5 ++ src/sat/bmc/bmcMaj9.c | 5 ++ 22 files changed, 419 insertions(+), 21 deletions(-) create mode 100644 src/misc/util/winsock_compat.h diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index 2d0894364..c9f5e2b4f 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -17,14 +17,6 @@ jobs: with: submodules: recursive - - name: Process project files to compile on Github Actions - run: | - sed -i 's#ABC_USE_PTHREADS\"#ABC_DONT_USE_PTHREADS\" /D \"_ALLOW_KEYWORD_MACROS=1\"#g' *.dsp - awk 'BEGIN { del=0; } /# Begin Group "uap"/ { del=1; } /# End Group/ { if( del > 0 ) {del=0; next;} } del==0 {print;} ' abclib.dsp > tmp.dsp - copy tmp.dsp abclib.dsp - del tmp.dsp - unix2dos *.dsp - - name: Prepare MSVC uses: bus1/cabuild/action/msdevshell@v1 with: @@ -32,20 +24,43 @@ jobs: - name: Upgrade project files to latest Visual Studio, ignoring upgrade errors, and build run: | - devenv abcspace.dsw /upgrade ; if (-not $? ) { cat UpgradeLog.htm } - msbuild abcspace.sln /m /nologo /p:Configuration=Release /p:PlatformTarget=x86 + 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' + } + 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_" + if ($LASTEXITCODE -ne 0) { throw "Build failed with exit code $LASTEXITCODE" } - name: Test Executable run: | - _TEST\abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + copy lib\x86\pthreadVC2.dll _TEST\ + .\_TEST\abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + if ($LASTEXITCODE -ne 0) { throw "Test failed with exit code $LASTEXITCODE" } - name: Stage Executable run: | - mkdir staging - copy _TEST/abc.exe staging/ - copy UpgradeLog.htm staging/ + mkdir staging + copy _TEST\abc.exe staging\ - - name: Upload pacakge artifact + - name: Upload package artifact uses: actions/upload-artifact@v4 with: name: package-windows diff --git a/abcexe.dsp b/abcexe.dsp index 9d5152fc2..80f0f1252 100644 --- a/abcexe.dsp +++ b/abcexe.dsp @@ -42,7 +42,7 @@ RSC=rc.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c -# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /c +# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -67,7 +67,7 @@ LINK32=link.exe # PROP Ignore_Export_Lib 0 # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c -# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /GZ /c +# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /GZ /c # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe diff --git a/abclib.dsp b/abclib.dsp index f7c80a25b..7b36b34e8 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -41,7 +41,7 @@ RSC=rc.exe # PROP Intermediate_Dir "ReleaseLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_MBCS" /D "_LIB" /YX /FD /c -# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /c +# ADD CPP /nologo /MD /W3 /GX /O2 /I "src" /D "WIN32" /D "WINDOWS" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /c # ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG" BSC32=bscmake.exe @@ -64,7 +64,7 @@ LIB32=link.exe -lib # PROP Intermediate_Dir "DebugLib" # PROP Target_Dir "" # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_MBCS" /D "_LIB" /YX /FD /GZ /c -# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /FR /YX /FD /GZ /c +# ADD CPP /nologo /MDd /W3 /Gm /GX /ZI /Od /I "src" /D "WIN32" /D "WINDOWS" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D ABC_DLL=ABC_DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_PTHREADS" /D "ABC_USE_CUDD" /D "HAVE_STRUCT_TIMESPEC" /D "_WINSOCKAPI_" /FR /YX /FD /GZ /c # ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG" BSC32=bscmake.exe @@ -513,6 +513,10 @@ SOURCE=.\src\base\abci\abcVerify.c SOURCE=.\src\base\abci\abcXsim.c # End Source File +# Begin Source File + +SOURCE=.\src\base\abci\abcTopo.c +# End Source File # End Group # Begin Group "cmd" @@ -709,6 +713,10 @@ SOURCE=.\src\base\io\ioWriteSmv.c SOURCE=.\src\base\io\ioWriteVerilog.c # End Source File +# Begin Source File + +SOURCE=.\src\base\io\ioJsonc.c +# End Source File # End Group # Begin Group "main" @@ -2153,6 +2161,18 @@ SOURCE=.\src\sat\bmc\bmcMulti.c SOURCE=.\src\sat\bmc\bmcUnroll.c # End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcMaj7.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcMaj8.c +# End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcMaj9.c +# End Source File # End Group # Begin Group "bsat2" @@ -3329,6 +3349,49 @@ SOURCE=.\src\opt\fxu\fxuSingle.c SOURCE=.\src\opt\fxu\fxuUpdate.c # End Source File +# Begin Group "untk" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\untk\NtkCmd.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\untk\Netlist.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\untk\NtkNtk.cpp +# End Source File +# End Group +# Begin Group "ufar" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarCmd.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarMgr.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarPth.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\ufar\UfarPth.h +# End Source File +# End Group +# Begin Group "util" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\util\util.cpp +# End Source File # End Group # Begin Group "rar" @@ -4445,6 +4508,10 @@ SOURCE=.\src\map\if\acd\ac_wrapper.cpp SOURCE=.\src\map\if\ifUtil.c # End Source File +# Begin Source File + +SOURCE=.\src\map\if\ifDecJ.c +# End Source File # End Group # Begin Group "amap" @@ -5021,6 +5088,30 @@ SOURCE=.\src\misc\util\utilSort.c SOURCE=.\src\misc\util\utilTruth.h # End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilBipart.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilLinear.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilMiniver.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilMulSim.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilAigSim.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilNet.c +# End Source File # End Group # Begin Group "nm" @@ -6241,6 +6332,22 @@ SOURCE=.\src\aig\gia\giaUnate.c SOURCE=.\src\aig\gia\giaUtil.c # End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaDecGraph.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaAgi.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaLutCas.c +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaMulFind3.c +# End Source File # End Group # Begin Group "miniaig" @@ -6474,7 +6581,6 @@ SOURCE=.\src\bool\rpo\rpo.c SOURCE=.\src\bool\rpo\rpo.h # End Source File # End Group -# End Group # Begin Group "prove" # PROP Default_Filter "" @@ -6570,6 +6676,7 @@ SOURCE=.\src\proof\cec\cecSweep.c SOURCE=.\src\proof\cec\cecSynth.c # End Source File # End Group +# End Group # Begin Group "dch" # PROP Default_Filter "" @@ -7213,12 +7320,14 @@ SOURCE=.\src\proof\acec\acecUtil.c SOURCE=.\src\proof\acec\acecXor.c # End Source File -# End Group + # End Group # End Group # Begin Group "Header Files" # PROP Default_Filter "h;hpp;hxx;hm;inl" # End Group +# End Group +# End Group # End Target # End Project diff --git a/src/aig/gia/giaLutCas.c b/src/aig/gia/giaLutCas.c index 340996565..dd18c7544 100644 --- a/src/aig/gia/giaLutCas.c +++ b/src/aig/gia/giaLutCas.c @@ -19,6 +19,10 @@ ***********************************************************************/ #include "gia.h" + +#ifdef _WIN32 +#include +#endif #include "sat/cnf/cnf.h" #include "misc/util/utilTruth.h" #include "sat/cadical/cadicalSolver.h" @@ -183,9 +187,13 @@ Gia_Man_t * Gia_ManGenLutCas( Gia_Man_t * p, char * pPermStr, int nVars, int nLu if ( Seed ) srand(Seed); else { +#ifdef _WIN32 + unsigned int seed = (unsigned int)GetTickCount(); +#else struct timespec ts; clock_gettime(CLOCK_REALTIME, &ts); unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec); +#endif srand(seed); } int fOwnPerm = (pPermStr == NULL); diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 3ab099655..fbe5c1f6c 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -31,8 +31,10 @@ #ifdef _WIN32 +#ifndef _MSC_VER #define inline __inline // compatible with MS VS 6.0 #endif +#endif /*---------------------------------------------------------------------------*/ /* Nested includes */ diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 5e1651d2e..c5a0327e0 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -31,7 +31,9 @@ #ifdef _WIN32 #ifndef __MINGW32__ +#ifndef _MSC_VER #define inline __inline // compatible with MS VS 6.0 +#endif #pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression #pragma warning(disable : 4200) // warning C4200: nonstandard extension used : zero-sized array in struct/union #pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data diff --git a/src/misc/util/utilAigSim.c b/src/misc/util/utilAigSim.c index a12d71d81..3bbde59a8 100644 --- a/src/misc/util/utilAigSim.c +++ b/src/misc/util/utilAigSim.c @@ -25,7 +25,44 @@ #include #include #include +#ifdef _WIN32 +#include +#define mkstemp(p) _mktemp_s(p, strlen(p)+1) +#else #include // mkstemp(), close(), unlink() +#endif + +#ifdef _WIN32 +// Windows doesn't have __builtin_ctzll, implement it using portable algorithm +static inline int __builtin_ctzll(uint64_t x) { + if (x == 0) return 64; + unsigned int n = 0; + if ((x & 0xFFFFFFFFULL) == 0) { + n += 32; + x >>= 32; + } + if ((x & 0xFFFFULL) == 0) { + n += 16; + x >>= 16; + } + if ((x & 0xFFULL) == 0) { + n += 8; + x >>= 8; + } + if ((x & 0xFULL) == 0) { + n += 4; + x >>= 4; + } + if ((x & 0x3ULL) == 0) { + n += 2; + x >>= 2; + } + if ((x & 0x1ULL) == 0) { + n += 1; + } + return n; +} +#endif #define AIGSIM_LIBRARY_ONLY @@ -147,6 +184,17 @@ static AigMan* Aig_ManLoadAigerBinary(const char *filename, int verbose) { static inline uint64_t u64_mask_n(int nBits) { return (nBits >= 64) ? ~0ull : ((nBits <= 0) ? 0ull : ((1ull << nBits) - 1ull)); } + +#ifdef _WIN32 +// Windows doesn't support __int128, so we limit to 32 variables on Windows +static void u128_to_dec(uint64_t x, char *buf, size_t cap) { + char tmp[64]; int n = 0; + if (!x) { snprintf(buf, cap, "0"); return; } + while (x && n < (int)sizeof(tmp)) { tmp[n++] = (char)('0' + (unsigned)(x % 10)); x /= 10; } + int k = 0; while (n && k + 1 < (int)cap) buf[k++] = tmp[--n]; + buf[k] = 0; +} +#else static void u128_to_dec(unsigned __int128 x, char *buf, size_t cap) { char tmp[64]; int n = 0; if (!x) { snprintf(buf, cap, "0"); return; } @@ -154,6 +202,7 @@ static void u128_to_dec(unsigned __int128 x, char *buf, size_t cap) { int k = 0; while (n && k + 1 < (int)cap) buf[k++] = tmp[--n]; buf[k] = 0; } +#endif enum { NW = 64, BATCH = NW * 64 }; // 4096 patterns/round @@ -334,7 +383,16 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, const uint64_t inMask = u64_mask_n(p1->nCis); const uint64_t outMask = u64_mask_n(p1->nCos); +#ifdef _WIN32 + // Windows doesn't support __int128, limit to 32 variables + if (nVars > 32) { + fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars); + return 0; + } + const uint64_t combs = ((uint64_t)1) << (unsigned)nVars; +#else const unsigned __int128 combs = ((unsigned __int128)1) << (unsigned)nVars; +#endif uint32_t *co1 = ABC_ALLOC(uint32_t, p1->nCos); uint32_t *co2 = ABC_ALLOC(uint32_t, p2->nCos); @@ -348,12 +406,21 @@ static int SimulateCompareAigAig(const AigMan *p1, const AigMan *p2, uint64_t inVec[BATCH], valid[NW]; unsigned long long rounds = 0; +#ifdef _WIN32 + uint64_t patsDone = 0; +#else unsigned __int128 patsDone = 0; +#endif clock_t t0 = clock(); +#ifdef _WIN32 + for (uint64_t base = 0; base < combs; base += BATCH) { + uint64_t remain = combs - base; +#else for (unsigned __int128 base = 0; base < combs; base += BATCH) { unsigned __int128 remain = combs - base; +#endif int nThis = (remain < BATCH) ? (int)remain : BATCH; int left = nThis; @@ -454,7 +521,16 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, const uint64_t inMask = u64_mask_n(p1->nCis); const uint64_t outMask = u64_mask_n(p1->nCos); +#ifdef _WIN32 + // Windows doesn't support __int128, limit to 32 variables + if (nVars > 32) { + fprintf(stderr, "Error: Windows build supports nVars<=32 (got nVars=%d)\n", nVars); + return 0; + } + const uint64_t combs = ((uint64_t)1) << (unsigned)nVars; +#else const unsigned __int128 combs = ((unsigned __int128)1) << (unsigned)nVars; +#endif // Precompute AIG CO literals uint32_t *co1 = ABC_ALLOC(uint32_t, p1->nCos); @@ -475,12 +551,21 @@ static int SimulateCompareAigBin(const AigMan *p1, const char *bin, uint64_t inVec[BATCH], valid[NW]; unsigned long long rounds = 0; +#ifdef _WIN32 + uint64_t patsDone = 0; +#else unsigned __int128 patsDone = 0; +#endif clock_t t0 = clock(); +#ifdef _WIN32 + for (uint64_t base = 0; base < combs; base += BATCH) { + uint64_t remain = combs - base; +#else for (unsigned __int128 base = 0; base < combs; base += BATCH) { unsigned __int128 remain = combs - base; +#endif int nThis = (remain < BATCH) ? (int)remain : BATCH; int left = nThis; diff --git a/src/misc/util/utilNet.c b/src/misc/util/utilNet.c index db21c8c3b..5d3173bb8 100755 --- a/src/misc/util/utilNet.c +++ b/src/misc/util/utilNet.c @@ -22,7 +22,11 @@ #include #include #include +#ifdef _WIN32 +#include +#else #include +#endif #include #include "abc_global.h" @@ -1083,7 +1087,11 @@ tn_vi * Tn_ParseSolution( const char * pFileName ) assert( 0 ); } fclose( pFile ); +#ifdef _WIN32 + _unlink( pFileName ); +#else unlink( pFileName ); +#endif return vRes; } tn_vi * Tn_SolveSat( const char * pFileNameIn, const char * pFileNameOut, int Seed, int TimeOut, int fVerbose ) diff --git a/src/misc/util/utilPrefix.cpp b/src/misc/util/utilPrefix.cpp index 50db0723c..cde54a42e 100644 --- a/src/misc/util/utilPrefix.cpp +++ b/src/misc/util/utilPrefix.cpp @@ -37,6 +37,7 @@ #include #include #include +#include //#include //#include //#include diff --git a/src/misc/util/utilPth.c b/src/misc/util/utilPth.c index aeb912597..940f7929a 100644 --- a/src/misc/util/utilPth.c +++ b/src/misc/util/utilPth.c @@ -23,6 +23,22 @@ #include #include +#ifdef _WIN32 +#include +#include +// nanosleep implementation for Windows +static inline int nanosleep(const struct timespec *req, struct timespec *rem) { + LARGE_INTEGER li; + li.QuadPart = -((LONGLONG)req->tv_sec * 10000000 + req->tv_nsec / 100); + HANDLE timer = CreateWaitableTimer(NULL, TRUE, NULL); + if (!timer) return -1; + SetWaitableTimer(timer, &li, 0, NULL, NULL, 0); + WaitForSingleObject(timer, INFINITE); + CloseHandle(timer); + return 0; +} +#endif + #ifdef ABC_USE_PTHREADS #ifdef _WIN32 @@ -35,7 +51,23 @@ #include using namespace std; #else +#ifndef _WIN32 #include +#else +// MSVC doesn't have stdatomic.h, use Interlocked functions instead +#define atomic_bool volatile LONG +#define atomic_int volatile LONG +#define atomic_store(obj, val) InterlockedExchange((LONG*)obj, val) +#define atomic_load(obj) (*(volatile LONG*)obj) +#define atomic_compare_exchange_strong(obj, expected, desired) \ + (InterlockedCompareExchange((LONG*)obj, desired, *expected) == *expected ? \ + (*expected = desired, 1) : (*expected = *(volatile LONG*)obj, 0)) +#define atomic_store_explicit(obj, val, order) InterlockedExchange((LONG*)obj, val) +#define atomic_load_explicit(obj, order) (*(volatile LONG*)obj) +#define memory_order_acquire 0 +#define memory_order_release 0 +#define memory_order_seq_cst 0 +#endif #include #endif diff --git a/src/misc/util/winsock_compat.h b/src/misc/util/winsock_compat.h new file mode 100644 index 000000000..501ec5d43 --- /dev/null +++ b/src/misc/util/winsock_compat.h @@ -0,0 +1,22 @@ +/* + * winsock_compat.h + * + * Compatibility header for timeval on Windows + * This must be included BEFORE windows.h to prevent winsock.h forward declaration conflicts + */ + +#ifndef SRC_MISC_UTIL_WINSOCK_COMPAT_H_ +#define SRC_MISC_UTIL_WINSOCK_COMPAT_H_ + +#ifdef _WIN32 + +// Define timeval before windows.h includes winsock.h +// This prevents winsock.h from forward declaring it as an incomplete type +struct timeval { + long tv_sec; + long tv_usec; +}; + +#endif /* _WIN32 */ + +#endif /* SRC_MISC_UTIL_WINSOCK_COMPAT_H_ */ \ No newline at end of file diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp index 162105c40..5bedeeca6 100755 --- a/src/opt/ufar/UfarCmd.cpp +++ b/src/opt/ufar/UfarCmd.cpp @@ -5,6 +5,12 @@ * Author: Yen-Sheng Ho */ +#ifdef _WIN32 +#include +#else +#include +#endif + #include #include #include diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp index ea565b5e4..924ad0d6b 100755 --- a/src/opt/ufar/UfarMgr.cpp +++ b/src/opt/ufar/UfarMgr.cpp @@ -14,7 +14,11 @@ #include #include +#ifdef _WIN32 +#include +#else #include +#endif #include #include diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h index dad82f6a2..ad2f9c477 100755 --- a/src/opt/ufar/UfarMgr.h +++ b/src/opt/ufar/UfarMgr.h @@ -15,7 +15,22 @@ #include #include #include +#ifdef _WIN32 +// Define timeval before windows.h to prevent winsock.h forward declaration conflicts +#ifndef _TIMEVAL_DEFINED +#define _TIMEVAL_DEFINED +struct timeval { + long tv_sec; + long tv_usec; +}; +#endif +#ifndef WIN32_LEAN_AND_MEAN +#define WIN32_LEAN_AND_MEAN +#endif +#include +#else #include +#endif #include "misc/util/abc_namespaces.h" diff --git a/src/opt/ufar/UfarPth.cpp b/src/opt/ufar/UfarPth.cpp index 6df45657f..f2ef59374 100755 --- a/src/opt/ufar/UfarPth.cpp +++ b/src/opt/ufar/UfarPth.cpp @@ -1,8 +1,12 @@ #include "misc/util/abc_namespaces.h" +#ifdef _WIN32 +#include "../lib/pthread.h" +#else #include #include +#endif #include "sat/bmc/bmc.h" #include "proof/pdr/pdr.h" diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 0ee5e5fd7..62ab1e343 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -5,8 +5,12 @@ * Author: Yen-Sheng Ho */ +#ifdef _WIN32 +#include +#else #include #include +#endif #include #include diff --git a/src/opt/util/util.cpp b/src/opt/util/util.cpp index df5de2fd8..a4b3ceba5 100644 --- a/src/opt/util/util.cpp +++ b/src/opt/util/util.cpp @@ -7,7 +7,11 @@ #include #include +#ifdef _WIN32 +#include +#else #include +#endif #ifdef __linux__ #include diff --git a/src/opt/util/util.h b/src/opt/util/util.h index 24dd153a1..2153e70d0 100755 --- a/src/opt/util/util.h +++ b/src/opt/util/util.h @@ -16,7 +16,37 @@ #include #include +#ifdef _WIN32 +// Define timeval before windows.h to prevent winsock.h forward declaration conflicts +#ifndef _TIMEVAL_DEFINED +#define _TIMEVAL_DEFINED +struct timeval { + long tv_sec; + long tv_usec; +}; +#endif +#ifndef WIN32_LEAN_AND_MEAN +#define WIN32_LEAN_AND_MEAN +#endif +#include + +static inline int gettimeofday(struct timeval *tv, struct timezone *tz) { + if (tv) { + FILETIME ft; + GetSystemTimeAsFileTime(&ft); + ULARGE_INTEGER uli; + uli.LowPart = ft.dwLowDateTime; + uli.HighPart = ft.dwHighDateTime; + ULONGLONG time_in_us = (uli.QuadPart - 116444736000000000ULL) / 10ULL; + tv->tv_sec = (long)(time_in_us / 1000000ULL); + tv->tv_usec = (long)(time_in_us % 1000000ULL); + } + (void)tz; + return 0; +} +#else #include +#endif #include "misc/util/abc_namespaces.h" diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c index 89b680684..3a65f17dd 100644 --- a/src/proof/ssw/sswPart.c +++ b/src/proof/ssw/sswPart.c @@ -26,7 +26,20 @@ #ifdef ABC_USE_PTHREADS #ifdef _WIN32 +#include +#include #include "../lib/pthread.h" +// nanosleep implementation for Windows +static inline int nanosleep(const struct timespec *req, struct timespec *rem) { + LARGE_INTEGER li; + li.QuadPart = -((LONGLONG)req->tv_sec * 10000000 + req->tv_nsec / 100); + HANDLE timer = CreateWaitableTimer(NULL, TRUE, NULL); + if (!timer) return -1; + SetWaitableTimer(timer, &li, 0, NULL, NULL, 0); + WaitForSingleObject(timer, INFINITE); + CloseHandle(timer); + return 0; +} #else #include #include @@ -36,7 +49,23 @@ #include using namespace std; #else +#ifndef _WIN32 #include +#else +// MSVC doesn't have stdatomic.h, use Interlocked functions instead +#define atomic_bool volatile LONG +#define atomic_int volatile LONG +#define atomic_store(obj, val) InterlockedExchange((LONG*)obj, val) +#define atomic_load(obj) (*(volatile LONG*)obj) +#define atomic_compare_exchange_strong(obj, expected, desired) \ + (InterlockedCompareExchange((LONG*)obj, desired, *expected) == *expected ? \ + (*expected = desired, 1) : (*expected = *(volatile LONG*)obj, 0)) +#define atomic_store_explicit(obj, val, order) InterlockedExchange((LONG*)obj, val) +#define atomic_load_explicit(obj, order) (*(volatile LONG*)obj) +#define memory_order_acquire 0 +#define memory_order_release 0 +#define memory_order_seq_cst 0 +#endif #include #endif diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index b82f35777..1b05c7605 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -27,6 +27,10 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _WIN32 +#include +#endif + ABC_NAMESPACE_IMPL_START @@ -1084,9 +1088,13 @@ Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize, int Seed ) if ( Seed ) srand(Seed); else { +#ifdef _WIN32 + unsigned int seed = (unsigned int)GetTickCount(); +#else struct timespec ts; clock_gettime(CLOCK_REALTIME, &ts); unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec); +#endif srand(seed); } for ( int i = 0; i < 1000; i++ ) { diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index a80f97330..b0c5391a9 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -27,6 +27,11 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _WIN32 +#include +typedef __int64 int64_t; +#endif + #define KISSAT_UNSAT 20 #define KISSAT_SAT 10 #define KISSAT_UNDEC 0 diff --git a/src/sat/bmc/bmcMaj9.c b/src/sat/bmc/bmcMaj9.c index cc15c153a..ea8ac9d17 100644 --- a/src/sat/bmc/bmcMaj9.c +++ b/src/sat/bmc/bmcMaj9.c @@ -27,7 +27,12 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" +#ifdef _WIN32 +#include +typedef __int64 int64_t; +#else #include +#endif #include #define KISSAT_UNSAT 20 From cdcfb2febfce8809fe41871287d8aab72d7ff75c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 21 Jan 2026 08:18:01 +0700 Subject: [PATCH 2/5] Changing some default return values to make sure scripts do not abort. --- src/base/abci/abc.c | 4 ++-- src/base/io/io.c | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0cecf8fc9..89c1b0751 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35427,7 +35427,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGiaBest == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" ); - return 1; + return 0; } Gia_ManPrintStats( pAbc->pGiaBest, pPars ); } @@ -35436,7 +35436,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" ); - return 1; + return 0; } Gia_ManPrintStats( pAbc->pGia, pPars ); } diff --git a/src/base/io/io.c b/src/base/io/io.c index d841bdb52..6d81d3a45 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -4207,7 +4207,7 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pAbc->pGia == NULL ) { Abc_Print( -1, "IoCommandWriteTruths(): There is no AIG.\n" ); - return 1; + return 0; } if ( Gia_ManPiNum(pAbc->pGia) > 16 ) { From d1157cae399c577453572de7d8c3c1c17a05528e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 25 Jan 2026 22:27:28 +0700 Subject: [PATCH 3/5] Updating the extension reading the arrival/required times. --- src/aig/gia/giaAiger.c | 44 +++++++++++++++++-------- src/aig/gia/giaLf.c | 4 +-- src/aig/gia/giaMan.c | 34 +++++++++++++++++--- src/aig/gia/giaTim.c | 10 ++++-- src/misc/tim/tim.h | 4 +-- src/misc/tim/timMan.c | 73 ++++++++++++++++++++++++++++++++++-------- 6 files changed, 131 insertions(+), 38 deletions(-) diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 85b48b118..6339b057f 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -649,23 +649,35 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi { pCur++; nInputs = Gia_AigerReadInt(pCur)/4; pCur += 4; + int nPiFf = Gia_ManPiNum(pNew) + Gia_ManRegNum(pNew); + if ( nInputs > nPiFf ) { + printf( "Warning: Timing info size (%d) exceeds PIs+FFs (%d). Using first %d values.\n", nInputs, nPiFf, nPiFf ); + nInputs = nPiFf; + } + else if ( nInputs > Gia_ManPiNum(pNew) && nInputs < nPiFf ) { + printf( "Warning: Timing info size (%d) is between PIs (%d) and PIs+FFs (%d). Using first %d values.\n", nInputs, Gia_ManPiNum(pNew), nPiFf, Gia_ManPiNum(pNew) ); + nInputs = Gia_ManPiNum(pNew); + } pNew->vInArrs = Vec_FltStart( nInputs ); memcpy( Vec_FltArray(pNew->vInArrs), pCur, (size_t)4*nInputs ); pCur += 4*nInputs; if ( fVerbose ) printf( "Finished reading extension \"i\".\n" ); - //if ( Vec_FltSize(pNew->vInArrs) == Gia_ManPiNum(pNew) ) - // Vec_FltFillExtra(pNew->vInArrs, Gia_ManCiNum(pNew), 0); - //assert( Vec_FltSize(pNew->vInArrs) == Gia_ManCiNum(pNew) ); } else if ( *pCur == 'o' ) { pCur++; nOutputs = Gia_AigerReadInt(pCur)/4; pCur += 4; + int nPoFf = Gia_ManPoNum(pNew) + Gia_ManRegNum(pNew); + if ( nOutputs > nPoFf ) { + printf( "Warning: Required time size (%d) exceeds POs+FFs (%d). Using first %d values.\n", nOutputs, nPoFf, nPoFf ); + nOutputs = nPoFf; + } + else if ( nOutputs > Gia_ManPoNum(pNew) && nOutputs < nPoFf ) { + printf( "Warning: Required time size (%d) is between POs (%d) and POs+FFs (%d). Using first %d values.\n", nOutputs, Gia_ManPoNum(pNew), nPoFf, Gia_ManPoNum(pNew) ); + nOutputs = Gia_ManPoNum(pNew); + } pNew->vOutReqs = Vec_FltStart( nOutputs ); memcpy( Vec_FltArray(pNew->vOutReqs), pCur, (size_t)4*nOutputs ); pCur += 4*nOutputs; if ( fVerbose ) printf( "Finished reading extension \"o\".\n" ); - //if ( Vec_FltSize(pNew->vOutReqs) == Gia_ManPoNum(pNew) ) - // Vec_FltFillExtra(pNew->vOutReqs, Gia_ManCoNum(pNew), 0); - //assert( Vec_FltSize(pNew->vOutReqs) == Gia_ManCoNum(pNew) ); } // read equivalence classes else if ( *pCur == 'e' ) @@ -1429,23 +1441,27 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in if ( p->pManTime ) { float * pTimes; - pTimes = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime ); + pTimes = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime, Gia_ManRegNum(p) ); if ( pTimes ) { + int nPis = Tim_ManPiNum((Tim_Man_t *)p->pManTime); + int nFlops = Gia_ManRegNum(p); fprintf( pFile, "i" ); - Gia_FileWriteBufferSize( pFile, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime) ); - fwrite( pTimes, 1, 4*Tim_ManPiNum((Tim_Man_t *)p->pManTime), pFile ); + Gia_FileWriteBufferSize( pFile, 4*(nPis + nFlops) ); + fwrite( pTimes, 1, 4*(nPis + nFlops), pFile ); ABC_FREE( pTimes ); - if ( fVerbose ) printf( "Finished writing extension \"i\".\n" ); + if ( fVerbose ) printf( "Finished writing extension \"i\" (PIs+Flops).\n" ); } - pTimes = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime ); + pTimes = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime, Gia_ManRegNum(p) ); if ( pTimes ) { + int nPos = Tim_ManPoNum((Tim_Man_t *)p->pManTime); + int nFlops = Gia_ManRegNum(p); fprintf( pFile, "o" ); - Gia_FileWriteBufferSize( pFile, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime) ); - fwrite( pTimes, 1, 4*Tim_ManPoNum((Tim_Man_t *)p->pManTime), pFile ); + Gia_FileWriteBufferSize( pFile, 4*(nPos + nFlops) ); + fwrite( pTimes, 1, 4*(nPos + nFlops), pFile ); ABC_FREE( pTimes ); - if ( fVerbose ) printf( "Finished writing extension \"o\".\n" ); + if ( fVerbose ) printf( "Finished writing extension \"o\" (POs+Flops).\n" ); } } // write equivalences diff --git a/src/aig/gia/giaLf.c b/src/aig/gia/giaLf.c index 130660050..006ac18f4 100644 --- a/src/aig/gia/giaLf.c +++ b/src/aig/gia/giaLf.c @@ -2306,8 +2306,8 @@ Gia_Man_t * Gia_ManPerformLfMapping( Gia_Man_t * p, Jf_Par_t * pPars, int fNorma Gia_ManTransferTiming( pNew, p ); p = pNew; // set arrival and required times - pPars->pTimesArr = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime ); - pPars->pTimesReq = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime ); + pPars->pTimesArr = Tim_ManGetArrTimes( (Tim_Man_t *)p->pManTime, Gia_ManRegNum(p) ); + pPars->pTimesReq = Tim_ManGetReqTimes( (Tim_Man_t *)p->pManTime, Gia_ManRegNum(p) ); } else p = Gia_ManDup( p ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index b60874601..889a49c0e 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -1033,15 +1033,28 @@ Vec_Int_t * Gia_ManDfsArrivals( Gia_Man_t * p, Vec_Int_t * vObjs ) Vec_Int_t * vTimes = Vec_IntStartFull( Gia_ManObjNum(p) ); Gia_Obj_t * pObj; int j, Entry, k, iFan; Vec_IntWriteEntry( vTimes, 0, 0 ); - if ( pManTime ) + if ( pManTime ) { Tim_ManIncrementTravId( pManTime ); Gia_ManForEachCi( p, pObj, j ) + { + float arrTime = 0; if ( j < Tim_ManPiNum(pManTime) ) { - float arrTime = Tim_ManGetCiArrival( pManTime, j ); + // PIs - direct index + arrTime = Tim_ManGetCiArrival( pManTime, j ); Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObj), (int)arrTime ); } + else if ( j >= Tim_ManCiNum(pManTime) - Gia_ManRegNum(p) ) + { + // Flops - need to remap index: stored at Tim_ManPiNum + flop_index + int flopIndex = j - (Tim_ManCiNum(pManTime) - Gia_ManRegNum(p)); + int remappedIndex = Tim_ManPiNum(pManTime) + flopIndex; + arrTime = Tim_ManGetCiArrival( pManTime, remappedIndex ); + Vec_IntWriteEntry( vTimes, Gia_ObjId(p, pObj), (int)arrTime ); + } + // BoxOutputs in the middle are skipped (no timing set) + } } else { @@ -1115,17 +1128,28 @@ Vec_Int_t * Gia_ManDfsRequireds( Gia_Man_t * p, Vec_Int_t * vObjs, int ReqTime ) Gia_Obj_t * pObj; int j, Entry, k, iFan, Req; Vec_IntWriteEntry( vTimes, 0, 0 ); - if ( pManTime ) + if ( pManTime ) { - int nCoLimit = Gia_ManCoNum(p) - Tim_ManPoNum(pManTime); Tim_ManIncrementTravId( pManTime ); //Tim_ManInitPoRequiredAll( pManTime, (float)ReqTime ); Gia_ManForEachCo( p, pObj, j ) - if ( j >= nCoLimit ) + { + if ( j < Gia_ManPoNum(p) ) { + // POs - direct index works since they come first Tim_ManSetCoRequired( pManTime, j, ReqTime ); Gia_ManDfsUpdateRequired( vTimes, Gia_ObjFaninId0p(p, pObj), ReqTime ); } + else if ( j >= Gia_ManCoNum(p) - Gia_ManRegNum(p) ) + { + // Flop inputs - remap index: stored at Tim_ManPoNum + flop_index + int flopIndex = j - (Gia_ManCoNum(p) - Gia_ManRegNum(p)); + int remappedIndex = Tim_ManPoNum(pManTime) + flopIndex; + Tim_ManSetCoRequired( pManTime, remappedIndex, ReqTime ); + Gia_ManDfsUpdateRequired( vTimes, Gia_ObjFaninId0p(p, pObj), ReqTime ); + } + // BoxInputs in the middle are skipped (no required time set) + } } else { diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 54012bbde..cb48d1de9 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -372,8 +372,14 @@ Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p ) Synopsis [Duplicates AIG according to the timing manager.] - Description [] - + Description [Converts a normalized AIG to unnormalized form for box processing. + In normalized AIG: CIs are ordered as PIs + BoxOutputs + FlopOutputs + In unnormalized AIG: CIs are ordered as PIs + FlopOutputs only, + with BoxOutputs spread throughout the AIG in topological order. + This transformation allows proper timing-aware processing of boxes. + For sequential AIGs, flop count is preserved, with flop outputs + remaining as CIs and flop inputs as COs.] + SideEffects [] SeeAlso [] diff --git a/src/misc/tim/tim.h b/src/misc/tim/tim.h index a01d53e32..3ab54335e 100644 --- a/src/misc/tim/tim.h +++ b/src/misc/tim/tim.h @@ -135,8 +135,8 @@ extern Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres ); extern Tim_Man_t * Tim_ManReduce( Tim_Man_t * p, Vec_Int_t * vBoxesLeft, int nTermsDiff ); extern Vec_Int_t * Tim_ManAlignTwo( Tim_Man_t * pSpec, Tim_Man_t * pImpl ); extern void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * vOutReqs ); -extern float * Tim_ManGetArrTimes( Tim_Man_t * p ); -extern float * Tim_ManGetReqTimes( Tim_Man_t * p ); +extern float * Tim_ManGetArrTimes( Tim_Man_t * p, int nRegs ); +extern float * Tim_ManGetReqTimes( Tim_Man_t * p, int nRegs ); extern void Tim_ManStop( Tim_Man_t * p ); extern void Tim_ManStopP( Tim_Man_t ** p ); extern void Tim_ManPrint( Tim_Man_t * p ); diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 9bcdaaae6..b90cb0b4d 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -449,6 +449,7 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * Vec_PtrWriteEntry( p->vDelayTables, pBox->iDelayTable, pTable ); } // create arrival times +/* if ( vInArrs ) { if ( Vec_FltSize(vInArrs) == Tim_ManPiNum(p) ) { @@ -461,21 +462,37 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * } else assert( 0 ); } +*/ + if ( vInArrs ) + { + assert( Vec_FltSize(vInArrs) >= Tim_ManPiNum(p) ); + if ( Vec_FltSize(vInArrs) == Tim_ManPiNum(p) ) { + Tim_ManForEachPi( p, pObj, i ) + pObj->timeArr = Vec_FltEntry(vInArrs, i); + } + else { + float Num; + Vec_FltForEachEntry( vInArrs, Num, i ) + p->pCis[i].timeArr = Num; + } + } + // create required times + // Handles: POs only, POs+Flops (partial COs), or all COs if ( vOutReqs ) { - k = 0; + assert( Vec_FltSize(vOutReqs) >= Tim_ManPoNum(p) ); if ( Vec_FltSize(vOutReqs) == Tim_ManPoNum(p) ) { + k = 0; Tim_ManForEachPo( p, pObj, i ) pObj->timeReq = Vec_FltEntry(vOutReqs, k++); assert( k == Tim_ManPoNum(p) ); } - else if ( Vec_FltSize(vOutReqs) == Tim_ManCoNum(p) ) { - Tim_ManForEachCo( p, pObj, i ) - pObj->timeReq = Vec_FltEntry(vOutReqs, k++); - assert( k == Tim_ManCoNum(p) ); + else { + float Num; + Vec_FltForEachEntry( vOutReqs, Num, i ) + p->pCos[i].timeReq = Num; } - else assert( 0 ); } } @@ -491,35 +508,65 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t * SeeAlso [] ***********************************************************************/ -float * Tim_ManGetArrTimes( Tim_Man_t * p ) +float * Tim_ManGetArrTimes( Tim_Man_t * p, int nRegs ) { float * pTimes; Tim_Obj_t * pObj; int i; + // Check if any PIs have non-zero arrival times Tim_ManForEachPi( p, pObj, i ) if ( pObj->timeArr != 0.0 ) break; - if ( i == Tim_ManPiNum(p) ) + if ( i == Tim_ManPiNum(p) && 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 ) + break; + if ( i == Tim_ManCiNum(p) ) + return NULL; // No timing info at all + } + else if ( i == Tim_ManPiNum(p) ) return NULL; - pTimes = ABC_FALLOC( float, Tim_ManCiNum(p) ); + // Allocate array for PIs + Flops (compact format, no box outputs) + pTimes = ABC_FALLOC( float, Tim_ManPiNum(p) + nRegs ); + // Copy PI timings Tim_ManForEachPi( p, pObj, i ) pTimes[i] = pObj->timeArr; + // Copy flop timings (from the end of CI array) + for ( i = 0; i < nRegs; i++ ) + pTimes[Tim_ManPiNum(p) + i] = p->pCis[Tim_ManCiNum(p) - nRegs + i].timeArr; return pTimes; } -float * Tim_ManGetReqTimes( Tim_Man_t * p ) +float * Tim_ManGetReqTimes( Tim_Man_t * p, int nRegs ) { float * pTimes; Tim_Obj_t * pObj; int i, k = 0; + // Check if any POs have non-infinity required times Tim_ManForEachPo( p, pObj, i ) if ( pObj->timeReq != TIM_ETERNITY ) break; - if ( i == Tim_ManPoNum(p) ) + if ( i == Tim_ManPoNum(p) && 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 ) + break; + if ( i == Tim_ManCoNum(p) ) + return NULL; // No timing info at all + } + else if ( i == Tim_ManPoNum(p) ) return NULL; - pTimes = ABC_FALLOC( float, Tim_ManCoNum(p) ); + // Allocate array for POs + Flops (compact format, no box inputs) + pTimes = ABC_FALLOC( float, Tim_ManPoNum(p) + nRegs ); + // Copy PO timings Tim_ManForEachPo( p, pObj, i ) - pTimes[k++] = pObj->timeArr; + pTimes[k++] = pObj->timeReq; assert( k == Tim_ManPoNum(p) ); + // Copy flop timings (from the end of CO array) + for ( i = 0; i < nRegs; i++ ) + pTimes[Tim_ManPoNum(p) + i] = p->pCos[Tim_ManCoNum(p) - nRegs + i].timeReq; return pTimes; } From dd21791031ea6b8965c1a5e8bf7d443fcdecfd19 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 Jan 2026 21:52:26 +0700 Subject: [PATCH 4/5] Extending &verify to handle combinational designs. --- src/aig/gia/giaDup.c | 44 ++++++++++++++++++-- src/aig/gia/giaTim.c | 10 +++++ src/misc/tim/timMan.c | 97 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 147 insertions(+), 4 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index c393f9519..84ed665f0 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5816,10 +5816,12 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla /**Function************************************************************* - Synopsis [] + Synopsis [Adds a dummy flop to the design.] + + Description [Duplicates the AIG while adding one flop with constant 0 input + and no fanout. Handles designs with boxes by also duplicating + the timing manager with an additional CI/CO pair.] - Description [] - SideEffects [] SeeAlso [] @@ -5827,11 +5829,13 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla ***********************************************************************/ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) { + extern Tim_Man_t * Tim_ManDupAddFlop( Tim_Man_t * p, int fUnitDelay ); Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 ); pNew->pName = Abc_UtilStrsav(p->pName); + pNew->pSpec = Abc_UtilStrsav(p->pSpec); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi( pNew ); @@ -5840,8 +5844,40 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); Gia_ManForEachCo( p, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManAppendCo( pNew, 0 ); + Gia_ManAppendCo( pNew, 0 ); Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)+1 ); + if ( p->pManTime ) + pNew->pManTime = Tim_ManDupAddFlop( (Tim_Man_t *)p->pManTime, 0 ); + if ( p->pAigExtra ) + pNew->pAigExtra = Gia_ManDup( p->pAigExtra ); + if ( p->vCiArrs ) + { + pNew->vCiArrs = Vec_IntDup( p->vCiArrs ); + Vec_IntPush( pNew->vCiArrs, 0.0 ); // default arrival for new flop output + } + if ( p->vCoReqs ) + { + pNew->vCoReqs = Vec_IntDup( p->vCoReqs ); + Vec_IntPush( pNew->vCoReqs, ABC_INFINITY ); // default required for new flop input + } + if ( p->vCoArrs ) + { + pNew->vCoArrs = Vec_IntDup( p->vCoArrs ); + Vec_IntPush( pNew->vCoArrs, 0.0 ); // default arrival for new flop input + } + if ( p->vCoAttrs ) + { + pNew->vCoAttrs = Vec_IntDup( p->vCoAttrs ); + Vec_IntPush( pNew->vCoAttrs, 0 ); // default attribute for new flop input + } + // copy other timing-related fields + pNew->And2Delay = p->And2Delay; + if ( p->vInArrs ) + pNew->vInArrs = Vec_FltDup( p->vInArrs ); + if ( p->vOutReqs ) + pNew->vOutReqs = Vec_FltDup( p->vOutReqs ); + pNew->DefInArrs = p->DefInArrs; + pNew->DefOutReqs = p->DefOutReqs; return pNew; } diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index cb48d1de9..080c74471 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -1128,6 +1128,16 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS // compute the miter if ( fSeq ) { + extern Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ); + if ( Gia_ManRegNum(pGia0) == 0 ) { + pGia0 = Gia_ManDupAddFlop( pMiter = pGia0 ); + Gia_ManStop( pMiter ); + } + if ( Gia_ManRegNum(pGia1) == 0 ) { + pGia1 = Gia_ManDupAddFlop( pMiter = pGia1 ); + Gia_ManStop( pMiter ); + } + pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose ); if ( pMiter ) { diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index b90cb0b4d..2df6007cc 100644 --- a/src/misc/tim/timMan.c +++ b/src/misc/tim/timMan.c @@ -152,6 +152,103 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the timing manager while adding one flop.] + + Description [Creates a new timing manager with one additional CI/CO pair + for a new flop. The new CI and CO are added at the end, + after all box inputs/outputs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Tim_Man_t * Tim_ManDupAddFlop( Tim_Man_t * p, int fUnitDelay ) +{ + Tim_Man_t * pNew; + Tim_Box_t * pBox; + Tim_Obj_t * pObj; + float * pDelayTable, * pDelayTableNew; + int i, k, nInputs, nOutputs; + + // clear traversal IDs + Tim_ManForEachCi( p, pObj, i ) + pObj->TravId = 0; + Tim_ManForEachCo( p, pObj, i ) + pObj->TravId = 0; + + // create new manager with one additional CI and CO + pNew = Tim_ManStart( p->nCis + 1, p->nCos + 1 ); + + // copy existing CI connectivity information + memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis ); + + // Initialize the new CI (flop output) + pNew->pCis[p->nCis].Id = p->nCis; + pNew->pCis[p->nCis].iObj2Box = -1; + pNew->pCis[p->nCis].iObj2Num = -1; + pNew->pCis[p->nCis].timeArr = 0.0; + pNew->pCis[p->nCis].timeReq = TIM_ETERNITY; + + // copy existing CO connectivity information + memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos ); + + // Initialize the new CO (flop input) + pNew->pCos[p->nCos].Id = p->nCos; + pNew->pCos[p->nCos].iObj2Box = -1; + pNew->pCos[p->nCos].iObj2Num = -1; + pNew->pCos[p->nCos].timeArr = 0.0; + pNew->pCos[p->nCos].timeReq = TIM_ETERNITY; + + if ( fUnitDelay ) + { + // clear PI arrival and PO required + Tim_ManInitPiArrivalAll( pNew, 0.0 ); + Tim_ManInitPoRequiredAll( pNew, (float)TIM_ETERNITY ); + } + + // duplicate delay tables + if ( Tim_ManDelayTableNum(p) > 0 ) + { + pNew->vDelayTables = Vec_PtrStart( Vec_PtrSize(p->vDelayTables) ); + Tim_ManForEachTable( p, pDelayTable, i ) + { + if ( pDelayTable == NULL ) + continue; + assert( i == (int)pDelayTable[0] ); + nInputs = (int)pDelayTable[1]; + nOutputs = (int)pDelayTable[2]; + pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs ); + pDelayTableNew[0] = (int)pDelayTable[0]; + pDelayTableNew[1] = (int)pDelayTable[1]; + pDelayTableNew[2] = (int)pDelayTable[2]; + for ( k = 0; k < nInputs * nOutputs; k++ ) + if ( pDelayTable[3+k] == -ABC_INFINITY ) + pDelayTableNew[3+k] = -ABC_INFINITY; + else + pDelayTableNew[3+k] = fUnitDelay ? (float)fUnitDelay : pDelayTable[3+k]; + assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL ); + Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew ); + } + } + + // duplicate boxes + if ( Tim_ManBoxNum(p) > 0 ) + { + pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) ); + Tim_ManForEachBox( p, pBox, i ) + { + Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs, + pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable, pBox->fBlack ); + Tim_ManBoxSetCopy( pNew, i, pBox->iCopy ); + } + } + + return pNew; +} + /**Function************************************************************* Synopsis [Trims the timing manager.] From 71e163571a551ea45bdbc65108f8071e9ca6558d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 Jan 2026 22:03:41 +0700 Subject: [PATCH 5/5] Rename ID mapping switch in &verify. --- src/base/abci/abc.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 89c1b0751..73c723a90 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43122,7 +43122,7 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) char * pFileSpec = NULL; int c, nBTLimit = 1000, nTimeLim = 0, fSeq = 0, fObjIdMap = 0, fDumpFiles = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTsmdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTsydvh" ) ) != EOF ) { switch ( c ) { @@ -43151,7 +43151,7 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': fSeq ^= 1; break; - case 'm': + case 'y': fObjIdMap ^= 1; break; case 'd': @@ -43176,12 +43176,12 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] \n" ); + Abc_Print( -2, "usage: &verify [-CT num] [-sydvh] \n" ); Abc_Print( -2, "\t performs verification of combinational design\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nTimeLim ); Abc_Print( -2, "\t-s : toggle using sequential verification [default = %s]\n", fSeq? "yes":"no"); - Abc_Print( -2, "\t-m : toggle producing object ID mapping (CEC only) [default = %s]\n", fObjIdMap? "yes":"no"); + Abc_Print( -2, "\t-y : toggle producing object ID mapping (CEC only) [default = %s]\n", fObjIdMap? "yes":"no"); Abc_Print( -2, "\t-d : toggle dumping AIGs to be compared [default = %s]\n", fDumpFiles? "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");