luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2026-01-28 09:37:06 +01:00
parent 01ad37aada 71e163571a
commit 9dcae29da3
31 changed files with 704 additions and 70 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
.github/workflows/build-windows.yml vendored
View File

@ -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 '<LanguageStandard>') {
$content = $content -replace '<LanguageStandard>Default</LanguageStandard>', '<LanguageStandard>stdcpp17</LanguageStandard>'
} else {
# Add LanguageStandard if it doesn't exist
$content = $content -replace '(<ClCompile>)', '$1<LanguageStandard>stdcpp17</LanguageStandard>'
}
Set-Content abclib.vcxproj -NoNewline $content
}
if (Test-Path abcexe.vcxproj) {
$content = Get-Content abcexe.vcxproj -Raw
if ($content -match '<LanguageStandard>') {
$content = $content -replace '<LanguageStandard>Default</LanguageStandard>', '<LanguageStandard>stdcpp17</LanguageStandard>'
} else {
# Add LanguageStandard if it doesn't exist
$content = $content -replace '(<ClCompile>)', '$1<LanguageStandard>stdcpp17</LanguageStandard>'
}
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

4
abcexe.dsp
View File

@ -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

117
abclib.dsp
View File

@ -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

44
src/aig/gia/giaAiger.c
View File

@ -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

44
src/aig/gia/giaDup.c
View File

@ -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;
}

4
src/aig/gia/giaLf.c
View File

@ -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 );

8
src/aig/gia/giaLutCas.c
View File

@ -19,6 +19,10 @@
***********************************************************************/
#include "gia.h"
#ifdef _WIN32
#include <windows.h>
#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);

34
src/aig/gia/giaMan.c
View File

@ -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
{

20
src/aig/gia/giaTim.c
View File

@ -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 []
@ -1122,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 )
{

12
src/base/abci/abc.c
View File

@ -35441,7 +35441,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 );
}
@ -35450,7 +35450,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 );
}
@ -43136,7 +43136,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 )
{
@ -43165,7 +43165,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':
@ -43190,12 +43190,12 @@ int Abc_CommandAbc9Verify( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &verify [-CT num] [-smdvh] <file>\n" );
Abc_Print( -2, "usage: &verify [-CT num] [-sydvh] <file>\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");

2
src/base/io/io.c
View File

@ -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 )
{

2
src/misc/extra/extra.h
View File

@ -31,8 +31,10 @@
#ifdef _WIN32
#ifndef _MSC_VER
#define inline __inline // compatible with MS VS 6.0
#endif
#endif
/*---------------------------------------------------------------------------*/
/* Nested includes */

4
src/misc/tim/tim.h
View File

@ -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 );

170
src/misc/tim/timMan.c
View File

@ -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.]
@ -449,6 +546,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 +559,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 +605,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;
}

2
src/misc/util/abc_global.h
View File

@ -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

85
src/misc/util/utilAigSim.c
View File

@ -25,9 +25,46 @@
#include <assert.h>
#include <ctype.h>
#include <time.h>
#ifdef _WIN32
#include <io.h>
#define mkstemp(p) _mktemp_s(p, strlen(p)+1)
#else
#include <unistd.h> // mkstemp(), close(), unlink()
#include <fcntl.h>
#include <sys/stat.h>
#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
@ -149,6 +186,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; }
@ -156,6 +204,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
@ -348,7 +397,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);
@ -362,12 +420,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;
@ -468,7 +535,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);
@ -489,12 +565,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;

8
src/misc/util/utilNet.c
View File

@ -22,7 +22,11 @@
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#ifdef _WIN32
#include <io.h>
#else
#include <unistd.h>
#endif
#include <time.h>
#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 )

1
src/misc/util/utilPrefix.cpp
View File

@ -37,6 +37,7 @@
#include <random>
#include <climits>
#include <iomanip>
#include <string>
//#include <cstdlib>
//#include <cstring>
//#include <cstdio>

32
src/misc/util/utilPth.c
View File

@ -23,6 +23,22 @@
#include <stdlib.h>
#include <assert.h>
#ifdef _WIN32
#include <windows.h>
#include <time.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;
}
#endif
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
@ -35,7 +51,23 @@
#include <atomic>
using namespace std;
#else
#ifndef _WIN32
#include <stdatomic.h>
#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 <stdbool.h>
#endif

22
src/misc/util/winsock_compat.h Normal file
View File

@ -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_ */

6
src/opt/ufar/UfarCmd.cpp
View File

@ -5,6 +5,12 @@
* Author: Yen-Sheng Ho
*/
#ifdef _WIN32
#include <windows.h>
#else
#include <sys/time.h>
#endif
#include <iostream>
#include <iomanip>
#include <climits>

4
src/opt/ufar/UfarMgr.cpp
View File

@ -14,6 +14,10 @@
#include <array>
#include <regex>
#ifdef _WIN32
#include <windows.h>
#endif
#include <base/wlc/wlc.h>
#include <sat/cnf/cnf.h>
#include <aig/gia/giaAig.h>

15
src/opt/ufar/UfarMgr.h
View File

@ -15,7 +15,22 @@
#include <sstream>
#include <iostream>
#include <memory>
#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 <windows.h>
#else
#include <sys/time.h>
#endif
#include "misc/util/abc_namespaces.h"

4
src/opt/ufar/UfarPth.cpp
View File

@ -1,8 +1,12 @@
#include "misc/util/abc_namespaces.h"
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#endif
#include "sat/bmc/bmc.h"
#include "proof/pdr/pdr.h"

4
src/opt/untk/NtkNtk.cpp
View File

@ -5,7 +5,11 @@
* Author: Yen-Sheng Ho
*/
#ifdef _WIN32
#include <windows.h>
#else
#include <unistd.h>
#endif
#include <fstream>
#include <base/wlc/wlc.h>

4
src/opt/util/util.cpp
View File

@ -9,7 +9,11 @@
#if !defined(__wasm)
#include <csignal>
#endif
#ifdef _WIN32
#include <windows.h>
#else
#include <unistd.h>
#endif
#ifdef __linux__
#include <sys/prctl.h>

30
src/opt/util/util.h
View File

@ -16,7 +16,37 @@
#include <map>
#include <vector>
#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 <windows.h>
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 <sys/time.h>
#endif
#include "misc/util/abc_namespaces.h"

29
src/proof/ssw/sswPart.c
View File

@ -26,7 +26,20 @@
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include <windows.h>
#include <time.h>
#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 <pthread.h>
#include <unistd.h>
@ -36,7 +49,23 @@
#include <atomic>
using namespace std;
#else
#ifndef _WIN32
#include <stdatomic.h>
#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 <stdbool.h>
#endif

8
src/sat/bmc/bmcMaj.c
View File

@ -27,6 +27,10 @@
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#ifdef _WIN32
#include <windows.h>
#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++ ) {

5
src/sat/bmc/bmcMaj8.c
View File

@ -27,6 +27,11 @@
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#ifdef _WIN32
#include <windows.h>
typedef __int64 int64_t;
#endif
#define KISSAT_UNSAT 20
#define KISSAT_SAT 10
#define KISSAT_UNDEC 0

5
src/sat/bmc/bmcMaj9.c
View File

@ -27,7 +27,12 @@
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#ifdef _WIN32
#include <windows.h>
typedef __int64 int64_t;
#else
#include <unistd.h>
#endif
#include <limits.h>
#define KISSAT_UNSAT 20