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 c9f5e2b4f..7b6e61304 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,47 @@ 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: Copy project files from scripts
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'
+ 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
+ $sourceFiles = [regex]::Matches($dspContent, 'SOURCE=\.\\([^\r\n]+)') | ForEach-Object { $_.Groups[1].Value } | Sort-Object -Unique
+
+ Write-Host "Found $($sourceFiles.Count) source files"
+
+ # Build source file items
+ $sourceItems = ""
+ foreach ($src in $sourceFiles) {
+ if ($src -match '\.c$') {
+ $sourceItems += " `r`n"
+ } elseif ($src -match '\.(cpp|cc)$') {
+ $sourceItems += " `r`n"
+ } elseif ($src -match '\.h$') {
+ $sourceItems += " `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_"
+
+ # 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
+
+ Write-Host "abclib.vcxproj 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
@@ -64,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
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\)'`
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/giaDup.c b/src/aig/gia/giaDup.c
index 0c0fd3d1e..d1187cb24 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( (char *)(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( (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 );
+ Gia_ManStop( pPart0 );
+
+ // Create Part 1 (top part: levels > Lcut)
+ pPart1 = Gia_ManStart( Gia_ManObjNum(p) );
+ pFileName = Extra_FileNameGenericAppend( (char *)(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( (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 );
+ Gia_ManStop( pPart1 );
+
+ // Clean up
+ Vec_IntFree( vCutNodes );
+ Vec_PtrFreeFree( vCutNames );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c
index 0c9d75098..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;
@@ -333,6 +336,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_ObjFanin0(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 )
@@ -381,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/base/abc/abcHieGia.c b/src/base/abc/abcHieGia.c
index 239f73ef1..ea3c2d09a 100644
--- a/src/base/abc/abcHieGia.c
+++ b/src/base/abc/abcHieGia.c
@@ -1292,12 +1292,203 @@ 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, "`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" );
+
+ 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" );
+ fprintf( pFile, "`endif\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 +1505,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 9b593370a..23c544823 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 );
@@ -680,6 +681,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 ///
////////////////////////////////////////////////////////////////////////
@@ -1501,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 );
@@ -34464,9 +34471,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 )
{
@@ -34479,6 +34486,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;
@@ -34541,17 +34551,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");
@@ -35118,15 +35149,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 )
{
@@ -35142,6 +35175,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;
@@ -35166,7 +35202,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 )
+ {
+ 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
{
@@ -35188,10 +35238,11 @@ 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");
@@ -42563,11 +42614,12 @@ 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;
char * pTemp;
+ char * pOrigFileName = NULL;
int fVerilog, fSystemVerilog;
*pAbc_ReadAigerOrVerilogFileStatus = 0;
@@ -42595,8 +42647,11 @@ 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\"",
+ "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;
@@ -42613,7 +42668,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;
}
@@ -42633,12 +42699,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 )
{
@@ -42673,6 +42739,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;
@@ -42794,7 +42869,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;
}
@@ -42830,7 +42905,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;
}
@@ -42942,11 +43017,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");
@@ -51334,10 +51410,11 @@ 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;
+ 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 )
{
@@ -51385,6 +51462,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;
@@ -51400,27 +51480,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" );
@@ -59402,7 +59511,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 );
@@ -59413,6 +59522,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 );
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 );
}
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index f028a1324..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 );
@@ -1722,7 +1723,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 +1990,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 +2125,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 );
@@ -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 )
{
@@ -3015,4 +3015,3 @@ void Wlc_MultBlastTest()
ABC_NAMESPACE_IMPL_END
-
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 c766fb7f1..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[k] != -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/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..45487af77 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),
@@ -974,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;
@@ -1076,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;
@@ -1359,8 +1380,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 +1403,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 +1455,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 +1464,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 +1481,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 +1495,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 +1505,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 +1524,8 @@ int UfarManager::PerformUIFProve(const timeval& timer) {
}
if (params.nGrey) {
+ if ( Ufar_ShouldStop(params) )
+ return -1;
DetermineGreyness(mem.pCex);
}
@@ -1509,6 +1550,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/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 0c74a4761..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
@@ -1119,7 +1122,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 +1149,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 +1250,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 +1269,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;
@@ -1284,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]));
@@ -1303,6 +1322,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::vectorvFlopClasses == 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" );
}
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/cec/cecProve.c b/src/proof/cec/cecProve.c
index 281dc2704..017296540 100644
--- a/src/proof/cec/cecProve.c
+++ b/src/proof/cec/cecProve.c
@@ -53,13 +53,19 @@ typedef struct Par_Share_t_ Par_Share_t;
typedef struct Par_ThData_t_ Par_ThData_t;
static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
+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 );
+
#ifndef ABC_USE_PTHREADS
-int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
+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 ) { return -1; }
#else // pthreads are used
#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;
@@ -74,8 +80,65 @@ typedef struct Par_ThData_t_
int nTimeOut;
int Result;
int fVerbose;
+ int nTimeOutU;
+ 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;
+ 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;
+ 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;
@@ -114,6 +177,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 );
@@ -143,6 +212,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 );
@@ -159,6 +229,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 );
@@ -176,6 +247,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 );
@@ -193,6 +265,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 );
@@ -212,6 +285,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 )
@@ -222,10 +304,17 @@ 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;
+ 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;
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 );
@@ -233,14 +322,21 @@ 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;
+ 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;
Cec_ManCorSetDefaultParams( pPars );
pPars->nBTLimit = 100;
pPars->nLevelMax = 100;
pPars->fVerbose = 0;
pPars->fUseCSat = 1;
+ pPars->pFunc = (void *)Cec_ScorrStop;
+ pPars->pData = (void *)&Stop;
return Cec_ManLSCorrespondence( p, pPars );
}
@@ -275,34 +371,37 @@ 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;
+ 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;
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 +411,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 = -1;
memset( &Share, 0, sizeof(Par_Share_t) );
Abc_CexFreeP( &p->pCexComb );
Abc_CexFreeP( &p->pCexSeq );
@@ -329,15 +428,16 @@ 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 );
+ 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, nProcs, p, RetValue, &RetEngine );
+ RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine );
if ( RetValue == -1 )
{
abctime clkScorr2, clkStart = Abc_Clock();
@@ -345,26 +445,26 @@ 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 )
+ 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, nProcs, p, RetValue, &RetEngine );
+ RetValue = 1, RetEngine = PAR_ENGINE_SCORR2;
+
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,18 +473,21 @@ 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;
}
if ( !fSilent )
{
- printf( "Problem \"%s\" is ", p->pSpec );
+ 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 );
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) )