diff --git a/.github/scripts/abcexe.vcxproj b/.github/scripts/abcexe.vcxproj new file mode 100644 index 0000000000..817e0809ef --- /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 0000000000..77498528db --- /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 0000000000..2c68905790 --- /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-mingw.yml b/.github/workflows/build-mingw.yml new file mode 100644 index 0000000000..f450380644 --- /dev/null +++ b/.github/workflows/build-mingw.yml @@ -0,0 +1,50 @@ +name: Build MinGW + +on: + push: + pull_request: + +jobs: + + build-mingw: + + runs-on: windows-latest + + defaults: + run: + shell: msys2 {0} + + steps: + + - name: Setup MSYS2 + uses: msys2/setup-msys2@v2 + with: + msystem: MINGW64 + update: false + install: >- + mingw-w64-x86_64-gcc + make + + - name: Git Checkout + uses: actions/checkout@v4 + with: + submodules: recursive + + - name: Build + run: | + ABC_USE_STDINT_H=1 make -j$(nproc) CFLAGS="-DWIN32 -DWIN32_NO_DLL" abc + + - name: Test Executable + run: | + ./abc.exe -c "r i10.aig; b; ps; b; rw -l; rw -lz; b; rw -lz; b; ps; cec" + + - name: Stage Executable + run: | + mkdir -p staging + cp abc.exe staging/ + + - name: Upload package artifact + uses: actions/upload-artifact@v4 + with: + name: package-mingw + path: staging/ diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index c9f5e2b4fa..7b6e613041 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' - } - 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' + 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 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 bef9a6aa4b..7236839d31 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 a9d9b79c51..dbf7198c4d 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) @@ -23,7 +30,11 @@ $(call abc_info,$(MSG_PREFIX)Using AR=$(AR)) $(call abc_info,$(MSG_PREFIX)Using LD=$(LD)) PROG := abc + OS := $(shell uname -s) +ifneq ($(filter MINGW%,$(OS)),) +OS := MINGW +endif MODULES := \ $(wildcard src/ext*) \ @@ -144,10 +155,15 @@ ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD NetBSD)) LIBS += -ldl endif -ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD NetBSD Darwin)) +ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD NetBSD Darwin MINGW)) LIBS += -lrt endif +# For PathMatchSpecA. +ifeq ($(OS), MINGW) + LIBS += -lshlwapi +endif + ifdef ABC_USE_LIBSTDCXX LIBS += -lstdc++ $(call abc_info,$(MSG_PREFIX)Using explicit -lstdc++) @@ -157,7 +173,7 @@ $(call abc_info,$(MSG_PREFIX)Using CFLAGS=$(CFLAGS)) CXXFLAGS += $(CFLAGS) -std=c++17 -fno-exceptions SRC := -GARBAGE := core core.* *.stackdump ./tags $(PROG) arch_flags +GARBAGE := core core.* *.stackdump ./tags $(PROG) arch_flags $(PROG).in .PHONY: all default tags clean docs cmake_info @@ -219,13 +235,22 @@ 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\)'` +ifeq ($(OS), MINGW) +$(PROG): $(OBJ) + @echo "$(MSG_PREFIX)\`\` Constructing Response File:" $(notdir @$@.in) + $(file >$@.in,$^ $(LDFLAGS) $(LIBS)) + @echo "$(MSG_PREFIX)\`\` Building binary:" $(notdir $@) + $(VERBOSE)$(LD) -o $@ @$@.in +else $(PROG): $(OBJ) @echo "$(MSG_PREFIX)\`\` Building binary:" $(notdir $@) $(VERBOSE)$(LD) -o $@ $^ $(LDFLAGS) $(LIBS) +endif lib$(PROG).a: $(LIBOBJ) @echo "$(MSG_PREFIX)\`\` Linking:" $(notdir $@) diff --git a/abclib.dsp b/abclib.dsp index 7b36b34e8f..321b851dfc 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -4510,6 +4510,10 @@ SOURCE=.\src\map\if\ifUtil.c # End Source File # Begin Source File +SOURCE=.\src\map\if\ifTrace.c +# End Source File +# Begin Source File + SOURCE=.\src\map\if\ifDecJ.c # End Source File # End Group diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index e9e9e67ca7..c37c3ea9e4 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 @@ -1289,7 +1297,7 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p ) Gia_AigerWriteUnsigned( vBuffer, uLit - uLit1 ); Gia_AigerWriteUnsigned( vBuffer, uLit1 - uLit0 ); } - Vec_StrPrintStr( vBuffer, "c" ); + Vec_StrPrintStr( vBuffer, "c\n" ); return vBuffer; } @@ -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 0c0fd3d1e1..d1187cb241 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/giaIf.c b/src/aig/gia/giaIf.c index e733bccad7..c2d8886c0a 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1190,7 +1190,7 @@ int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_ { word Truth; int i, iObjLit1, iObjLit2, iObjLit3; - word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1 ); + word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1, 0 ); assert( z != 0 ); if ( ((z >> 63) & 1) == 0 ) { @@ -2124,6 +2124,24 @@ void Gia_ManConfigPrint2( unsigned char * pConfigData, int nLeaves ) } } +static inline word Gia_ManFromIfPermuteTruth4( word Truth, int nLeaves, word z ) +{ + word TruthNew = 0; + int i, k, x; + assert( nLeaves >= 1 && nLeaves <= 4 ); + for ( i = 0; i < 16; i++ ) + { + x = 0; + for ( k = 0; k < nLeaves; k++ ) + { + int v = (int)((z >> (2 * k)) & 3); + x |= ((i >> k) & 1) << v; + } + TruthNew |= ((Truth >> x) & 1) << i; + } + return TruthNew; +} + /**Function************************************************************* Synopsis [Derive configurations.] @@ -2135,33 +2153,42 @@ void Gia_ManConfigPrint2( unsigned char * pConfigData, int nLeaves ) SeeAlso [] ***********************************************************************/ -void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * pTruth, int nLeaves ) +void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * pTruth, int nLeaves, int fDelay ) { int i, CellId; int startPos = Vec_StrSize(vConfigs2); + If_LibCell_t * pCellLib = pIfMan && pIfMan->pPars ? pIfMan->pPars->pCellLib : NULL; + assert( pCellLib != NULL ); // Determine cell type based on the number of leaves and configuration if ( nLeaves <= 4 ) // 7 bytes = 1 byte CellId + 4 bytes mapping + 2 bytes truth table { + word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1, fDelay ); + int fHavePerm = (z != 0) && ((z & ABC_CONST(0x4000000000000000)) != 0); + word Truth = pTruth[0]; // Cell type 0: Simple LUT4 CellId = 0; // Write CellId Vec_StrPush( vConfigs2, (char)CellId ); // Write mapping for ( i = 0; i < nLeaves; i++ ) - Vec_StrPush( vConfigs2, 2+i ); + { + int v = fHavePerm ? (int)((z >> (2 * i)) & 3) : i; + Vec_StrPush( vConfigs2, 2 + v ); + } for ( ; i < 4; i++ ) Vec_StrPush( vConfigs2, 0 ); // Write truth table (16 bits for LUT4) - word Truth = pTruth[0]; + if ( fHavePerm ) + Truth = Gia_ManFromIfPermuteTruth4( Truth, nLeaves, z ); Vec_StrPush( vConfigs2, (char)((Truth >> 8) & 0xFF) ); Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) ); - assert( startPos + 7 == Vec_StrSize(vConfigs2) ); + assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) ); //Gia_ManConfigPrint( Truth, 0, nLeaves ); } else // 12 bytes = 1 byte CellId + 7 bytes mapping + 4 bytes truth tables { - word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1 ); + word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1, fDelay ); //Gia_ManConfigPrint( 0, z, nLeaves ); if ( ((z >> 63) & 1) == 0 ) { @@ -2201,7 +2228,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) ); Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) ); Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) ); - assert( startPos + 12 == Vec_StrSize(vConfigs2) ); + assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) ); } else // 14 bytes = 1 byte CellId + 9 bytes mapping + 4 bytes truth tables { @@ -2226,7 +2253,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) ); Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) ); Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) ); - assert( startPos + 14 == Vec_StrSize(vConfigs2) ); + assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) ); } } if ( pIfMan->pPars->fVerboseTrace ) @@ -2551,7 +2578,16 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLeaves), k ); if ( Abc_LitIsCompl(pIfObj->iCopy) ^ pCutBest->fCompl ) Abc_TtNot( pTruth, Abc_TtWordNum(pCutBest->nLeaves) ); - Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pTruth, pCutBest->nLeaves ); + if ( pIfMan->pPars->fDelayOptCell ) + { + pIfMan->nCutLeavesCur = pCutBest->nLeaves; + If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k ) + { + pIfMan->pCutLeavesCur[k] = pIfLeaf->Id; + pIfMan->pCutLeafArrCur[k] = If_ObjCutBest(pIfLeaf)->Delay; + } + } + Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pTruth, pCutBest->nLeaves, pIfMan->pPars->fDelayOptCell ); } } else @@ -2964,6 +3000,20 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars ) pPars->pTimesReq[i] = EntryF; } */ + if ( p->pManTime && pPars->pTimesArr == NULL ) + { + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + pPars->pTimesArr = ABC_CALLOC( float, Gia_ManCiNum(p) ); + for ( i = 0; i < Gia_ManCiNum(p); i++ ) + pPars->pTimesArr[i] = Tim_ManGetCiArrival( pManTime, i ); + } + if ( p->pManTime && pPars->pTimesReq == NULL ) + { + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + pPars->pTimesReq = ABC_CALLOC( float, Gia_ManCoNum(p) ); + for ( i = 0; i < Gia_ManCoNum(p); i++ ) + pPars->pTimesReq[i] = Tim_ManGetCoRequired( pManTime, i ); + } ABC_FREE( p->pCellStr ); Vec_IntFreeP( &p->vConfigs ); Vec_StrFreeP( &p->vConfigs2 ); @@ -3337,4 +3387,3 @@ Gia_Man_t * Gia_ManDupUnhashMapping( Gia_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaLf.c b/src/aig/gia/giaLf.c index 006ac18f42..4f3e49f424 100644 --- a/src/aig/gia/giaLf.c +++ b/src/aig/gia/giaLf.c @@ -1838,6 +1838,12 @@ static inline int Lf_ManDerivePart( Lf_Man_t * p, Gia_Man_t * pNew, Vec_Int_t * } pTruth = Lf_CutTruth( p, pCut ); iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 ); + // do not create LUT in the simple case + if ( Abc_Lit2Var(iLit) == 0 ) + return iLit; + Vec_IntForEachEntry( vLeaves, iTemp, k ) + if ( Abc_Lit2Var(iLit) == Abc_Lit2Var(iTemp) ) + return iLit; // create mapping Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) ); Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) ); diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index 0c9d750989..6986c84185 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -33,6 +33,53 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static int Gia_ManConfig2GetBytePos( Gia_Man_t * p, int iObj, If_LibCell_t * pCellLib ) +{ + int iLut, bytePos = 0; + if ( p == NULL || p->vConfigs2 == NULL || pCellLib == NULL ) + return -1; + Gia_ManForEachLut( p, iLut ) + { + unsigned char CellId; + int nRecordSize; + if ( bytePos >= Vec_StrSize(p->vConfigs2) ) + return -1; + if ( iLut == iObj ) + return bytePos; + CellId = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos ); + if ( CellId >= IF_MAX_LUTSIZE ) + return -1; + nRecordSize = pCellLib->pCellRecordSizes[CellId]; + if ( nRecordSize <= 0 ) + return -1; + bytePos += nRecordSize; + } + return -1; +} +int Gia_ManConfig2DerivePinDelays( Gia_Man_t * p, int iObj, If_LibCell_t * pCellLib, int * pPinDelay, int nLutSize ) +{ + int bytePos, i, nPins; + unsigned char CellId; + if ( pCellLib == NULL || pPinDelay == NULL || nLutSize < 1 || nLutSize > 32 ) + return 0; + for ( i = 0; i < nLutSize; i++ ) + pPinDelay[i] = 1; + bytePos = Gia_ManConfig2GetBytePos( p, iObj, pCellLib ); + if ( bytePos < 0 || bytePos >= Vec_StrSize(p->vConfigs2) ) + return 0; + CellId = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos ); + if ( CellId >= pCellLib->nCellNum ) + return 0; + nPins = Abc_MinInt( pCellLib->nCellInputs[CellId], 9 ); + for ( i = 0; i < nPins; i++ ) + { + int v = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos + 1 + i ); + if ( v >= 2 && v < 2 + nLutSize ) + pPinDelay[v - 2] = Abc_MaxInt( pPinDelay[v - 2], pCellLib->pCellPinDelays[CellId][i] ); + } + return 1; +} + /**Function************************************************************* Synopsis [Sorts the pins in the decreasing order of delays.] @@ -113,7 +160,7 @@ float Gia_ObjComputeArrival( Gia_Man_t * p, int iObj, int fUseSorting ) If_LibLut_t * pLutLib = (If_LibLut_t *)p->pLutLib; If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib; Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); - int k, iFanin, pPinPerm[32]; + int k, iFanin, pPinPerm[32], pPinDelay[32]; float pPinDelays[32]; float tArrival, * pDelays; if ( Gia_ObjIsCi(pObj) ) @@ -132,15 +179,17 @@ float Gia_ObjComputeArrival( Gia_Man_t * p, int iObj, int fUseSorting ) { // Handle cell library delays (use integer delays directly) int nLutSize = Gia_ObjLutSize(p, iObj); + int fHaveCfg2 = Gia_ManConfig2DerivePinDelays( p, iObj, pCellLib, pPinDelay, nLutSize ); // Find matching cell (simple approach: use first cell with enough inputs) int cellId = -1; int i; - for ( i = 0; i < pCellLib->nCellNum; i++ ) - if ( pCellLib->nCellInputs[i] >= nLutSize ) - { - cellId = i; - break; - } + if ( !fHaveCfg2 ) + for ( i = 0; i < pCellLib->nCellNum; i++ ) + if ( pCellLib->nCellInputs[i] >= nLutSize ) + { + cellId = i; + break; + } if ( cellId >= 0 ) { // Use cell delays as integers from the library @@ -151,6 +200,15 @@ float Gia_ObjComputeArrival( Gia_Man_t * p, int iObj, int fUseSorting ) tArrival = Gia_ObjTimeArrival(p, iFanin) + delay; } } + else if ( fHaveCfg2 ) + { + Gia_LutForEachFanin( p, iObj, iFanin, k ) + { + float delay = (float)pPinDelay[k]; + if ( tArrival < Gia_ObjTimeArrival(p, iFanin) + delay ) + tArrival = Gia_ObjTimeArrival(p, iFanin) + delay; + } + } else { // Fall back to default delay if no matching cell @@ -204,11 +262,14 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting ) { If_LibLut_t * pLutLib = (If_LibLut_t *)p->pLutLib; If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib; - int k, iFanin, pPinPerm[32]; + int k, iFanin, pPinPerm[32], pPinDelay[32]; float pPinDelays[32]; 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; @@ -220,15 +281,17 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting ) { // Handle cell library delays (use integer delays directly) int nLutSize = Gia_ObjLutSize(p, iObj); + int fHaveCfg2 = Gia_ManConfig2DerivePinDelays( p, iObj, pCellLib, pPinDelay, nLutSize ); // Find matching cell (simple approach: use first cell with enough inputs) int cellId = -1; int i; - for ( i = 0; i < pCellLib->nCellNum; i++ ) - if ( pCellLib->nCellInputs[i] >= nLutSize ) - { - cellId = i; - break; - } + if ( !fHaveCfg2 ) + for ( i = 0; i < pCellLib->nCellNum; i++ ) + if ( pCellLib->nCellInputs[i] >= nLutSize ) + { + cellId = i; + break; + } if ( cellId >= 0 ) { // Use cell delays as integers from the library @@ -240,6 +303,15 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting ) Gia_ObjSetTimeRequired( p, iFanin, tRequired ); } } + else if ( fHaveCfg2 ) + { + Gia_LutForEachFanin( p, iObj, iFanin, k ) + { + tRequired = Gia_ObjTimeRequired( p, iObj ) - (float)pPinDelay[k]; + if ( Gia_ObjTimeRequired(p, iFanin) > tRequired ) + Gia_ObjSetTimeRequired( p, iFanin, tRequired ); + } + } else { // Fall back to default delay if no matching cell @@ -333,6 +405,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 +479,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; @@ -946,4 +1046,3 @@ Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerb ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abc/abcHieGia.c b/src/base/abc/abcHieGia.c index f2f6f8ca60..ea3c2d09a3 100644 --- a/src/base/abc/abcHieGia.c +++ b/src/base/abc/abcHieGia.c @@ -1333,6 +1333,7 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName ) fprintf( pFile, "`timescale 1ns/1ps\n\n" ); // Write LUT module definitions for Yosys compatibility (compact version) + fprintf( pFile, "`ifdef LUTSPECS\n" ); fprintf( pFile, "module LUT2 #( parameter INIT = 04\'h0 ) ( output O, input I0, I1 );\n" ); fprintf( pFile, " assign O = INIT[ {I1, I0} ];\n" ); fprintf( pFile, "endmodule\n" ); @@ -1351,7 +1352,8 @@ static void GiaHie_DumpMappedLuts( Gia_Man_t * p, char * pFileName ) fprintf( pFile, "module LUT6 #( parameter INIT = 64\'h0 ) ( output O, input I0, I1, I2, I3, I4, I5 );\n" ); fprintf( pFile, " assign O = INIT[ {I5, I4, I3, I2, I1, I0} ];\n" ); - fprintf( pFile, "endmodule\n\n" ); + fprintf( pFile, "endmodule\n" ); + fprintf( pFile, "`endif\n\n" ); // Write main module fprintf( pFile, "module " ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dbb5ed99e3..6cc8df18fc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -659,6 +659,7 @@ static int Abc_CommandAbc9MulFind3 ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9BsFind ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9AndCare ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cuts ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Divide ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1506,8 +1507,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mulfind3", Abc_CommandAbc9MulFind3, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bsfind", Abc_CommandAbc9BsFind, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&andcare", Abc_CommandAbc9AndCare, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&cuts", Abc_CommandAbc9Cuts, 0 ); - + Cmd_CommandAdd( pAbc, "ABC9", "&cuts", Abc_CommandAbc9Cuts, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "÷", Abc_CommandAbc9Divide, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 ); @@ -22283,7 +22285,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) If_ManSetDefaultPars( pPars ); pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut(); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYUZDEWSJqalepmrsdbgxyzuojiktncfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYZUDEWSJqalepmrsdbgxyzuoiktncfvh" ) ) != EOF ) { switch ( c ) { @@ -22533,9 +22535,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fUseBuffs ^= 1; break; - case 'j': - pPars->fEnableCheck07 ^= 1; - break; + //case 'j': + // pPars->fEnableCheck07 ^= 1; + // break; case 'i': pPars->fUseCofVars ^= 1; break; @@ -22865,7 +22867,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) sprintf(LutSize, "library" ); else sprintf(LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: if [-KCFAGRNTXYUZ num] [-DEW float] [-SJ str] [-qarlepmsdbgxyuojiktnczfvh]\n" ); + Abc_Print( -2, "usage: if [-KCFAGRNTXYZMU num] [-DEW float] [-SJ str] [-qarlepmsdbgxyuoiktnczfvh]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -22899,7 +22901,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" ); Abc_Print( -2, "\t-u : toggles delay optimization with SAT-based library [default = %s]\n", pPars->fUserSesLib? "yes": "no" ); Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" ); - Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); + //Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" ); Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" ); Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" ); Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" ); @@ -34455,9 +34457,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) Aig_Man_t * pAig; Gia_Man_t * pGia, * pTemp; char * pInits; - int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fVerbose = 0; + int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fReuseNames = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cmnvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cmnrvh" ) ) != EOF ) { switch ( c ) { @@ -34470,6 +34472,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'n': fNames ^= 1; break; + case 'r': + fReuseNames ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -34532,17 +34537,38 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) pGia->vOutReqs = Vec_FltAllocArray( Abc_NtkGetCoRequiredFloats(pNtk), Abc_NtkCoNum(pNtk) ); pGia->And2Delay = pNtk->AndGateDelay; } + if ( fReuseNames ) + { + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "There is no current AIG to reuse names from.\n" ); + return 1; + } + if ( Gia_ManCiNum(pGia) != Gia_ManCiNum(pAbc->pGia) ) + { + Abc_Print( -1, "The number of CIs differ.\n" ); + return 1; + } + if ( Gia_ManCoNum(pGia) != Gia_ManCoNum(pAbc->pGia) ) + { + Abc_Print( -1, "The number of COs differ.\n" ); + return 1; + } + ABC_SWAP( Vec_Ptr_t *, pGia->vNamesIn, pAbc->pGia->vNamesIn ); + ABC_SWAP( Vec_Ptr_t *, pGia->vNamesOut, pAbc->pGia->vNamesOut ); + } Abc_FrameUpdateGia( pAbc, pGia ); return 0; usage: - Abc_Print( -2, "usage: &get [-cmnvh] \n" ); + Abc_Print( -2, "usage: &get [-cmnrvh] \n" ); Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" ); Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" ); Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" ); Abc_Print( -2, "\t-c : toggles allowing simple GIA to be imported [default = %s]\n", fGiaSimple? "yes": "no" ); Abc_Print( -2, "\t-m : toggles preserving the current mapping [default = %s]\n", fMapped? "yes": "no" ); Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" ); + Abc_Print( -2, "\t-r : toggles reusing CI/CO names of the current AIG [default = %s]\n", fReuseNames? "yes": "no" ); Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the file name\n"); @@ -35163,7 +35189,7 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // Check if we should write LUT-based Verilog - if ( fUseLuts || (Gia_ManHasMapping(pAbc->pGia) && !fUseGates) ) + if ( fUseLuts ) { if ( !Gia_ManHasMapping(pAbc->pGia) ) { @@ -35206,7 +35232,6 @@ int Abc_CommandAbc9WriteVer( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t : the file name\n"); - Abc_Print( -2, "\tNote: When AIG is mapped and -l is not specified, LUT-based output is automatically used.\n"); return 1; } @@ -42575,11 +42600,12 @@ int Abc_CommandAbc9EquivFilter( Abc_Frame_t * pAbc, int argc, char ** argv ) SeeAlso [] ***********************************************************************/ -static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, int * pAbc_ReadAigerOrVerilogFileStatus ) +static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus ) { FILE * pFile; Gia_Man_t * pGia; char * pTemp; + char * pOrigFileName = NULL; int fVerilog, fSystemVerilog; *pAbc_ReadAigerOrVerilogFileStatus = 0; @@ -42605,11 +42631,20 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu fVerilog = fSystemVerilog || Extra_FileIsType( pFileName, ".v", NULL, NULL ); if ( fVerilog ) { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = NULL; char pCommand[2000]; int RetValue; + int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL ); + // Save the original filename before changing it + pOrigFileName = pFileName; snprintf( pCommand, sizeof(pCommand), - "yosys -qp \"read_verilog %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"", - fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" ); + "yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols _temp_.aig\"", + pDefines ? "-D" : "", pDefines ? pDefines : "", + (fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName, + pFileName2 ? " " : "", pFileName2 ? pFileName2 : "", + pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", + pFileName2 ? "delete t:\\$scopeinfo; " : "" ); #if defined(__wasm) RetValue = 1; #else @@ -42620,12 +42655,45 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand ); return NULL; } - pFileName = "_temp_.aig"; + if ( pFileName2 ) + { + Abc_Ntk_t * pNtk = Io_Read( "_temp_.aig", IO_FILE_AIGER, 1, 0 ); + if ( pNtk == NULL ) + { + Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", "_temp_.aig" ); + return NULL; + } + pAig = Abc_NtkToDar( pNtk, 0, 1 ); + Abc_NtkDelete( pNtk ); + if ( pAig == NULL ) + { + Abc_Print( -1, "Converting the AIGER network into an internal AIG has failed.\n" ); + return NULL; + } + pGia = Gia_ManFromAig( pAig ); + Aig_ManStop( pAig ); + } + else + { + pFileName = "_temp_.aig"; + pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); + } } - - pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); + else + 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; } @@ -42644,13 +42712,14 @@ 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; + FILE * pFile; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; - char ** pArgvNew, * pTopModule = NULL; + char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL, * pFileName2 = 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, "CTMDFnmdbasxytvwh" ) ) != EOF ) { switch ( c ) { @@ -42685,6 +42754,24 @@ 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 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + pFileName2 = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'n': pPars->fNaive ^= 1; break; @@ -42729,6 +42816,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 0, "It looks like the current AIG is derived by &st -m. Such AIG contains XOR gates and cannot be verified before &st is applied.\n" ); return 1; } + if ( pFileName2 ) + { + if ( (pFile = fopen( pFileName2, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\".\n", pFileName2 ); + return 1; + } + fclose( pFile ); + } pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; if ( fMiter ) @@ -42806,7 +42902,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], pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[n] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } @@ -42842,7 +42938,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, pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus ); if ( pGias[1] == NULL ) return Abc_ReadAigerOrVerilogFileStatus; } @@ -42954,11 +43050,13 @@ 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] [-F 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-F str : second Verilog/SystemVerilog file read together with each Verilog input [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"); @@ -44017,8 +44115,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameSetLibLut( If_LibLutSetSimple( 6 ) ); } pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut(); + pPars->pCellLib = (If_LibCell_t *)Abc_FrameReadLibCell(); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSJTXYZqalepmrsdbgxyofuijkztncvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSJTXYZMqalepmrsdbgxyofuijkztncvwh" ) ) != EOF ) { switch ( c ) { @@ -44034,6 +44133,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; // if the LUT size is specified, disable library pPars->pLutLib = NULL; + pPars->pCellLib = NULL; break; case 'C': if ( globalUtilOptind >= argc ) @@ -44123,6 +44223,21 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nAndDelay < 0 ) goto usage; break; + case 'M': + { + int Value; + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by 0 or 1.\n" ); + goto usage; + } + Value = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Value < 0 || Value > 1 ) + goto usage; + pPars->fDelayOptCell = Value; + break; + } case 'D': if ( globalUtilOptind >= argc ) { @@ -44299,6 +44414,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Auto-detected K=%d from cell library (max inputs).\n", nMaxInputs ); // Disable LUT library since we're using K from cell library pPars->pLutLib = NULL; + pPars->pCellLib = pCellLib; } } } @@ -44487,6 +44603,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nLutSize = 4; } + if ( pPars->fEnableCheck07 ) + pPars->nCutsMax = Abc_MaxInt( pPars->nCutsMax, 16 ); + else + pPars->pCellLib = NULL; + // enable truth table computation if cut minimization is selected if ( pPars->fCutMin || pPars->fDeriveLuts ) { @@ -44622,7 +44743,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) sprintf(LutSize, "library" ); else sprintf(LutSize, "%d", pPars->nLutSize ); - Abc_Print( -2, "usage: &if [-KCFAGRTXY num] [-DEW float] [-SJ str] [-qarlepmsdbgxyofuijkztnchvw]\n" ); + Abc_Print( -2, "usage: &if [-KCFAGRTXYZM num] [-DEW float] [-SJ str] [-qarlepmsdbgxyofuijkztnchvw]\n" ); Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax ); @@ -44633,6 +44754,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -2, "\t-T num : the type of LUT structures [default = any]\n", pPars->nStructType ); Abc_Print( -2, "\t-X num : delay of AND-gate in LUT library units [default = %d]\n", pPars->nAndDelay ); Abc_Print( -2, "\t-Y num : area of AND-gate in LUT library units [default = %d]\n", pPars->nAndArea ); + Abc_Print( -2, "\t-M num : enables delay-driven decomposition [default = %d]\n", pPars->fDelayOptCell ); Abc_Print( -2, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer ); Abc_Print( -2, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon ); Abc_Print( -2, "\t-W float : sets wire delay between adjects LUTs [default = %f]\n", pPars->WireDelay ); @@ -48535,22 +48657,13 @@ int Abc_CommandAbc9Trace( Abc_Frame_t * pAbc, int argc, char ** argv ) pAbc->pGia->pLutLib = fUseLutLib ? Abc_FrameReadLibLut() : NULL; pAbc->pGia->pCellLib = fUseCellLib ? Abc_FrameReadLibCell() : NULL; - if ( pFileName ) - { - // Dump the delay trace to file - Gia_ManDelayTraceDump( pAbc->pGia, (char *)pFileName ); - } - else - { - // Print the delay trace to console - Gia_ManDelayTraceLutPrint( pAbc->pGia, fVerbose ); - } + Gia_ManDelayTraceDump( pAbc->pGia, (char *)pFileName ); return 0; usage: Abc_Print( -2, "usage: &trace [-F file] [-lcvh]\n" ); Abc_Print( -2, "\t performs delay trace of LUT-mapped network\n" ); - Abc_Print( -2, "\t-F file : dump the critical path to a file [default = console output]\n" ); + Abc_Print( -2, "\t-F file : dump the critical path to a file [default = stdout]\n" ); Abc_Print( -2, "\t-l : toggle using LUT-library-delay model [default = %s]\n", fUseLutLib? "yes": "no" ); Abc_Print( -2, "\t-c : toggle using cell-library-delay model [default = %s]\n", fUseCellLib? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); @@ -51348,7 +51461,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { 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; + int c, nProcs = 6, nProcsNew = 0, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF ) { @@ -51360,10 +51473,11 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" ); goto usage; } - nProcs = atoi(argv[globalUtilOptind]); + nProcsNew = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nProcs <= 0 ) + if ( nProcsNew <= 0 || nProcsNew > 6 ) goto usage; + nProcs = nProcsNew; break; case 'T': if ( globalUtilOptind >= argc ) @@ -51461,7 +51575,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: 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-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs ); Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-U num : 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 ); @@ -59447,7 +59561,7 @@ int Abc_CommandAbc9Cuts( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: cuts [-KC num] [-tdbvh]\n" ); + Abc_Print( -2, "usage: &cuts [-KC num] [-tdbvh]\n" ); Abc_Print( -2, "\t computes K-input cuts for the nodes in the current AIG\n" ); Abc_Print( -2, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", 2, 14, nCutSize ); Abc_Print( -2, "\t-C num : max number of cuts at a node (%d <= num <= %d) [default = %d]\n", 2, 256, nCutNum ); @@ -59458,6 +59572,76 @@ int Abc_CommandAbc9Cuts( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 c4744ebe05..3ec0e929ac 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 fff4fa9f6b..aae2f47d8d 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -67,6 +67,7 @@ static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv static int CmdCommandStarter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandAutoTuner ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandSolver ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int CmdCommandSolver2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -97,6 +98,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "quit", CmdCommandQuit, 0 ); Cmd_CommandAdd( pAbc, "Basic", "abcrc", CmdCommandAbcrc, 0 ); Cmd_CommandAdd( pAbc, "Basic", "history", CmdCommandHistory, 0 ); + Cmd_CommandAdd( pAbc, "Basic", "hi", CmdCommandHistory, 0 ); Cmd_CommandAdd( pAbc, "Basic", "alias", CmdCommandAlias, 0 ); Cmd_CommandAdd( pAbc, "Basic", "unalias", CmdCommandUnalias, 0 ); Cmd_CommandAdd( pAbc, "Basic", "help", CmdCommandHelp, 0 ); @@ -123,6 +125,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "starter", CmdCommandStarter, 0 ); Cmd_CommandAdd( pAbc, "Various", "autotuner", CmdCommandAutoTuner, 0 ); Cmd_CommandAdd( pAbc, "Various", "&solver", CmdCommandSolver, 0 ); + Cmd_CommandAdd( pAbc, "Various", "&solver2", CmdCommandSolver2, 0 ); Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn, 0 ); } @@ -439,42 +442,83 @@ int CmdCommandAbcrc( Abc_Frame_t * pAbc, int argc, char **argv ) int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) { char * pName, * pStr = NULL; - int i, c; + char ** ppMatches = NULL; + int * pIds = NULL; + int i; int nPrints = 20; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + int nPrinted = 0; + if ( argc == 2 && !strcmp(argv[1], "-h") ) + goto usage; + if ( argc > 3 ) + goto usage; + // parse arguments: can be [substring] [number] in either order + if ( argc == 2 ) { - switch ( c ) + // one argument: either number or substring + pStr = argv[1]; + if ( pStr && pStr[0] >= '1' && pStr[0] <= '9' ) { - case 'h': - goto usage; - default : - goto usage; + nPrints = atoi(pStr); + pStr = NULL; } } - if ( argc > globalUtilOptind + 1 ) - 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; + else if ( argc == 3 ) + { + // two arguments: substring and number + char * arg1 = argv[1]; + char * arg2 = argv[2]; + + // 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 { - Vec_PtrForEachEntry( char *, pAbc->aHistory, pName, i ) + // Search string provided, select up to nPrints most recent matching entries + ppMatches = ABC_ALLOC( char *, nPrints ); + pIds = ABC_ALLOC( int, nPrints ); + Vec_PtrForEachEntryReverse( char *, pAbc->aHistory, pName, i ) if ( strstr(pName, pStr) ) - fprintf( pAbc->Out, "%2d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName ); + { + pIds[nPrinted] = Vec_PtrSize(pAbc->aHistory)-i; + ppMatches[nPrinted] = pName; + if ( ++nPrinted >= nPrints ) + break; + } + // Print the selected entries in reverse so larger history indices appear first + for ( i = nPrinted - 1; i >= 0; i-- ) + fprintf( pAbc->Out, "%4d : %s\n", pIds[i], ppMatches[i] ); + ABC_FREE( pIds ); + ABC_FREE( ppMatches ); } 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 ); } @@ -2931,6 +2975,79 @@ int CmdCommandSolver( Abc_Frame_t * pAbc, int argc, char **argv ) return 1; } + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int CmdCommandSolver2( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + FILE * pFile; + char Command[2000]; + int i; + + if ( argc > 1 ) + { + if ( strcmp( argv[1], "-h" ) == 0 ) + goto usage; + if ( strcmp( argv[1], "-?" ) == 0 ) + goto usage; + } + +#if defined(__wasm) + fprintf( pAbc->Err, "Unsupported command.\n" ); + return 1; +#else + // Check if solver binary exists in current directory or PATH + if ( (pFile = fopen( "./solver", "r" )) != NULL ) + { + sprintf( Command, "%s", "./solver" ); + fclose( pFile ); + } + else + { + char CheckCommand[100]; + sprintf( CheckCommand, "which solver > /dev/null 2>&1" ); + if ( system( CheckCommand ) != 0 ) + { + fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" ); + goto usage; + } + sprintf( Command, "%s", "solver" ); + } + + // Append user-provided arguments as-is: solver + for ( i = 1; i < argc; i++ ) + { + strcat( Command, " " ); + strcat( Command, argv[i] ); + } + + fprintf( pAbc->Out, "Executing command: %s\n", Command ); + if ( system( Command ) == -1 ) + { + fprintf( pAbc->Err, "The following command has failed:\n" ); + fprintf( pAbc->Err, "\"%s\"\n", Command ); + return 1; + } +#endif + return 0; + +usage: + fprintf( pAbc->Err, "\tusage: &solver2 \n"); + fprintf( pAbc->Err, "\t run the external solver as \"solver \"\n" ); + fprintf( pAbc->Err, "\t-h : print the command usage\n" ); + fprintf( pAbc->Err, "\t : all arguments passed directly to solver\n" ); + return 1; +} + /**Function******************************************************************** Synopsis [Print the version string.] diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index e8e28078f8..f0d8fc2dd5 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -25,7 +25,6 @@ #include ABC_NAMESPACE_IMPL_START - // proper declaration of isspace //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -393,9 +392,51 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop ) ***********************************************************************/ char * CmdHistorySubstitution( Abc_Frame_t * pAbc, char *line, int *changed ) { - // as of today, no history substitution - *changed = 0; - return line; + char * pBeg = line, * pEnd, * pStr; + int iRecall, nSize; + while ( *pBeg && isspace((unsigned char)*pBeg) ) + pBeg++; + if ( *pBeg == 0 ) + { + *changed = 0; + return line; + } + pEnd = pBeg; + while ( *pEnd && !isspace((unsigned char)*pEnd) ) + pEnd++; + if ( *pEnd ) + { + char * pTemp = pEnd; + while ( *pTemp && isspace((unsigned char)*pTemp) ) + pTemp++; + if ( *pTemp ) + { + *changed = 0; + return line; + } + } + if ( *pBeg < '1' || *pBeg > '9' ) + { + *changed = 0; + return line; + } + for ( pStr = pBeg; pStr < pEnd; pStr++ ) + if ( *pStr < '0' || *pStr > '9' ) + { + *changed = 0; + return line; + } + iRecall = atoi( pBeg ); + nSize = Vec_PtrSize( pAbc->aHistory ); + if ( iRecall < 1 || iRecall > nSize ) + { + fprintf( pAbc->Err, "History entry %d does not exist.\n", iRecall ); + line[0] = 0; + *changed = 0; + return line; + } + *changed = 1; + return (char *)Vec_PtrEntry( pAbc->aHistory, nSize - iRecall ); } /**Function************************************************************* @@ -905,4 +946,3 @@ void Cmd_CommandSGen( Abc_Frame_t * pAbc, int nParts, int nIters, int fVerbose ) /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index 3c5d67b3fe..9589d5239e 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -56,6 +56,7 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS. #endif #include "base/abc/abc.h" +#include "base/cmd/cmdInt.h" #include "mainInt.h" #include "base/wlc/wlc.h" @@ -363,9 +364,15 @@ int Abc_RealMain( int argc, char * argv[] ) // execute commands given by the user while ( !feof(stdin) ) { + int did_subst; // print command line prompt and // get the command from the user sCommand = Abc_UtilsGetUsersInput( pAbc ); + sCommand = CmdHistorySubstitution( pAbc, sCommand, &did_subst ); + if ( sCommand == NULL ) + break; + if ( did_subst ) + fprintf( pAbc->Out, "%s\n", sCommand ); // execute the user's command fStatus = Cmd_CommandExecute( pAbc, sCommand ); diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index 1b76fab8fc..2436932cd3 100644 --- a/src/base/wln/wlnCom.c +++ b/src/base/wln/wlnCom.c @@ -93,11 +93,12 @@ void Wln_End( Abc_Frame_t * pAbc ) int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ); - extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); + extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ); FILE * pFile; char * pFileName = NULL; + char * pFileName2= NULL; char * pTopModule= NULL; char * pDefines = NULL; char * pLibrary = NULL; @@ -111,7 +112,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSetUndef = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLbdisumlcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLFbdisumlcvh" ) ) != EOF ) { switch ( c ) { @@ -151,6 +152,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) pLibrary = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + pFileName2 = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'b': fBlast ^= 1; break; @@ -200,10 +210,24 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } fclose( pFile ); + if ( pFileName2 ) + { + if ( (pFile = fopen( pFileName2, "r" )) == NULL ) + { + Abc_Print( 1, "Cannot open input file \"%s\".\n", pFileName2 ); + return 0; + } + fclose( pFile ); + } // perform reading if ( pLibrary ) { + if ( pFileName2 ) + { + Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); + return 0; + } Abc_Ntk_t * pNtk = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose ); @@ -220,11 +244,18 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pNew = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + { + if ( pFileName2 ) + { + Abc_Print( 1, "Command line switch \"-F\" is only supported when the main input is Verilog/SystemVerilog.\n" ); + return 0; + } + pNew = Wln_BlastSystemVerilog( pFileName, NULL, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + } else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); @@ -234,6 +265,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { + if ( pFileName2 ) + { + Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); + return 0; + } Rtl_Lib_t * pLib = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); @@ -250,12 +286,13 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) } return 0; usage: - Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-bdisumlcvh] \n" ); + Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-F ] [-bdisumlcvh] \n" ); Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" ); Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" ); Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" ); Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" ); Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" ); + Abc_Print( -2, "\t-F : specify a second Verilog/SystemVerilog file for the default bit-blasting flow (default \"not used\")\n" ); Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" ); Abc_Print( -2, "\t-d : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" ); diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index 5b9f05c45c..ffe8e457d7 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -19,6 +19,9 @@ ***********************************************************************/ #include "wln.h" +#include "aig/aig/aig.h" +#include "aig/gia/giaAig.h" +#include "base/io/ioAbc.h" #include "base/main/main.h" #ifdef WIN32 @@ -171,30 +174,54 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p unlink( pFileTemp ); return pNtk; } -Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) +Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) { Gia_Man_t * pGia = NULL; char Command[1000]; char * pFileTemp = "_temp_.aig"; int fRtlil = strstr(pFileName, ".rtl") != NULL; - int fSVlog = strstr(pFileName, ".sv") != NULL; - sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols %s\"", + int fSVlog = strstr(pFileName, ".sv") != NULL || (pFileName2 && strstr(pFileName2, ".sv") != NULL); + sprintf( Command, "%s -qp \"%s %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", Wln_GetYosysName(), fRtlil ? "read_rtlil" : "read_verilog", pDefines ? "-D" : "", pDefines ? pDefines : "", fSVlog ? "-sv " : "", pFileName, + pFileName2 ? " " : "", + pFileName2 ? pFileName2 : "", pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "", fSetUndef ? "setundef -init -zero; " : "", + pFileName2 ? "delete t:\\$scopeinfo; " : "", pFileTemp ); if ( fVerbose ) printf( "%s\n", Command ); if ( !Wln_ConvertToRtl(Command, pFileTemp) ) return NULL; - pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 ); + if ( pFileName2 ) + { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = NULL; + Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); + if ( pNtk == NULL ) + { + printf( "Reading AIGER from file \"%s\" has failed.\n", pFileTemp ); + return NULL; + } + pAig = Abc_NtkToDar( pNtk, 0, 1 ); + Abc_NtkDelete( pNtk ); + if ( pAig == NULL ) + { + printf( "Converting the AIGER network into an internal AIG has failed.\n" ); + return NULL; + } + pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig); + Aig_ManStop( pAig ); + } + else + pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 ); if ( pGia == NULL ) { printf( "Converting to AIG has failed.\n" ); diff --git a/src/map/if/if.h b/src/map/if/if.h index 3f9ddd101b..a76b66268f 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -126,6 +126,7 @@ struct If_Par_t_ int fCutMin; // performs cut minimization by removing functionally reducdant variables int fDelayOpt; // special delay optimization int fDelayOptLut; // delay optimization for LUTs + int fDelayOptCell; // delay optimization for cells int fDsdBalance; // special delay optimization int fUserRecLib; // use recorded library int fUserSesLib; // use SAT-based synthesis @@ -175,6 +176,7 @@ struct If_Par_t_ float FinalDelay; // final delay after mapping float FinalArea; // final area after mapping If_LibLut_t * pLutLib; // the LUT library + If_LibCell_t * pCellLib; // the cell library float * pTimesArr; // arrival times float * pTimesReq; // required times int (* pFuncCost) (If_Man_t *, If_Cut_t *); // procedure to compute the user's cost of a cut @@ -201,6 +203,7 @@ struct If_LibCell_t_ char * pName; // the name of the LUT library int nCellNum; // the number of cells in the library int nCellInputs[IF_MAX_LUTSIZE]; + int pCellRecordSizes[IF_MAX_LUTSIZE]; char * pCellNames[IF_MAX_LUTSIZE]; float pCellAreas[IF_MAX_LUTSIZE]; int pCellPinDelays[IF_MAX_LUTSIZE][IF_MAX_LUTSIZE]; @@ -299,6 +302,14 @@ struct If_Man_t_ Vec_Int_t * vVisited2; Vec_Int_t * vCuts; Vec_Int_t * vCutCosts; + // current cut context for user callbacks + If_Obj_t * pCutObjCur; // current object whose cut is being checked + If_Cut_t * pCutCur; // current cut being checked + int nCutLeavesCur; // number of leaves in current cut + int pCutLeavesCur[IF_MAX_LUTSIZE]; // current cut leaves (IDs) + float pCutLeafArrCur[IF_MAX_LUTSIZE]; // current cut leaf arrivals + float CutDelayCur; // current cut delay returned by user callback + int fCutDelayCurValid; // indicates CutDelayCur is valid // timing manager Tim_Man_t * pManTim; @@ -319,6 +330,7 @@ struct If_Cut_t_ float Edge; // the edge flow float Power; // the power flow float Delay; // delay of the cut + word Config; // configuration string int iCutFunc; // TT ID of the cut int uMaskFunc; // polarity bitmask unsigned uSign; // cut signature @@ -564,7 +576,8 @@ extern float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj extern float If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot ); /*=== ifDec.c =============================================================*/ extern word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); -extern word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive ); +extern word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive, int fDelay ); +extern void If_CutComputeIntrinsicJ( If_Man_t * p, word Config, int nLeaves, int * pIntrinsicDelays ); extern int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern int If_CutPerformCheck08( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); extern int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr ); @@ -741,4 +754,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c index 58649b7204..975a573068 100644 --- a/src/map/if/ifCore.c +++ b/src/map/if/ifCore.c @@ -207,4 +207,3 @@ int If_ManPerformMappingComb( If_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/map/if/ifDecJ.c b/src/map/if/ifDecJ.c index 018ad49691..61b5c744f7 100644 --- a/src/map/if/ifDecJ.c +++ b/src/map/if/ifDecJ.c @@ -1,6 +1,6 @@ /**CFile**************************************************************** - FileName [ifDec07.c] + FileName [ifDecJ.c] SystemName [ABC: Logic synthesis and verification system.] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - November 21, 2006.] - Revision [$Id: ifDec07.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] + Revision [$Id: ifDecJ.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -35,14 +35,14 @@ int If_CutPerformCheckJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves { return 1; } -word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive ) +word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive, int fDelay ) { return 0; } -void If_PermUnpack( unsigned Value, int Pla2Var[9] ) +void If_CutComputeIntrinsicJ( If_Man_t * p, word Config, int nLeaves, int * pIntrinsicDelays ) { } -void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName ) +void If_PermUnpack( unsigned Value, int Pla2Var[9] ) { } @@ -52,4 +52,3 @@ void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName ) ABC_NAMESPACE_IMPL_END - diff --git a/src/map/if/ifLibLut.c b/src/map/if/ifLibLut.c index ee819a2a1f..afb44e680c 100644 --- a/src/map/if/ifLibLut.c +++ b/src/map/if/ifLibLut.c @@ -388,6 +388,39 @@ If_LibCell_t * If_LibCellAlloc( void ) return p; } +/**Function************************************************************* + + Synopsis [Computes the record size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static int If_LibCellComputeRecordSize( char * pFuncDesc, int nInputs ) +{ + int i, nMapBytes, nRecordSize; + assert( pFuncDesc != NULL ); + nMapBytes = (Abc_Base2Log(nInputs + 2) + 7) / 8; + nRecordSize = 1 + nInputs * nMapBytes; + for ( i = 0; pFuncDesc[i]; i++ ) + { + int nLutVars = 0; + if ( pFuncDesc[i] != '{' ) + continue; + for ( i++; pFuncDesc[i] && pFuncDesc[i] != '}'; i++ ) + if ( pFuncDesc[i] >= 'a' && pFuncDesc[i] <= 'z' ) + nLutVars++; + assert( nLutVars < 31 ); + nRecordSize += ((1 << nLutVars) + 7) / 8; + if ( pFuncDesc[i] == 0 ) + break; + } + return nRecordSize; +} + /**Function************************************************************* Synopsis [Reads the description of cells from the cell library file.] @@ -471,6 +504,7 @@ If_LibCell_t * If_LibCellRead( char * FileName ) nInputs = maxChar - 'a' + 1; } p->nCellInputs[CellId] = nInputs; + p->pCellRecordSizes[CellId] = If_LibCellComputeRecordSize( FuncDesc, nInputs ); // Read Area pToken = strtok( NULL, " \t\n" ); diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 1a79014da4..ba5601fe85 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -226,7 +226,7 @@ void If_ManSimpleSort( int * pArray, int nSize ) void If_ManDumpCut( If_Cut_t * pCut, int nLutSize, Vec_Int_t * vCuts ) { int i; - for ( i = 0; i < pCut->nLeaves; i++ ) + for ( i = 0; i < (int)pCut->nLeaves; i++ ) Vec_IntPush( vCuts, pCut->pLeaves[i] ); for ( ; i < nLutSize; i++ ) Vec_IntPush( vCuts, -1 ); @@ -719,6 +719,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId ) pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] ); pCut->iCutFunc = p->pPars->fUseTtPerm ? 3 : (p->pPars->fTruth ? 2: -1); pCut->uMaskFunc = 0; + pCut->Config = 0; assert( pCut->pLeaves[0] < p->vObjs->nSize ); } diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index ac62e26e43..f93b73edb0 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -162,12 +162,13 @@ int * If_CutArrTimeProfile( If_Man_t * p, If_Cut_t * pCut ) void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess, int fFirst ) { If_Set_t * pCutSet; + If_Obj_t * pLeaf; If_Cut_t * pCut0, * pCut1, * pCut; If_Cut_t * pCut0R, * pCut1R; int fFunc0R, fFunc1R; int i, k, v, iCutDsd, fChange; int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUserLutDec || p->pPars->fUserLut2D || - p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2 || p->pPars->fUseCheck1 || p->pPars->fUseCheck2; + p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2 || p->pPars->fUseCheck1 || p->pPars->fUseCheck2 || p->pPars->fEnableCheck07; int fUseAndCut = (p->pPars->nAndDelay > 0) || (p->pPars->nAndArea > 0); assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 ); assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 ); @@ -193,6 +194,30 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL ); else if ( p->pPars->fDsdBalance ) pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL ); + else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell ) + { + int iLeaf, Intrinsic[IF_MAX_LUTSIZE]; + float Delay = -IF_FLOAT_LARGE; + if ( pCut->nLeaves == 0 ) + { + pCut->fUseless = 0; + pCut->Delay = 0.0; + goto IfMapBestCutDone; + } + assert( pCut->nLeaves == 1 || pCut->Config ); + If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic ); + If_CutForEachLeaf( p, pCut, pLeaf, iLeaf ) + { + If_Cut_t * pBestCut = If_ObjCutBest( pLeaf ); + assert( pBestCut != NULL ); + assert( pBestCut->fUseless == 0 ); + Delay = IF_MAX( Delay, If_ObjArrTime(pLeaf) + (float)Intrinsic[iLeaf] ); + } + pCut->fUseless = (Delay > IF_FLOAT_LARGE/2); + pCut->Delay = Delay; +IfMapBestCutDone: + ; + } else if ( p->pPars->fUserRecLib ) pCut->Delay = If_CutDelayRecCost3( p, pCut, pObj ); else if ( p->pPars->fUserSesLib ) @@ -268,7 +293,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep if ( !If_CutMergeOrdered( p, pCut0, pCut1, pCut ) ) continue; } - if ( p->pPars->fUserLutDec && !fFirst && pCut->nLeaves > p->pPars->nLutDecSize ) + if ( p->pPars->fUserLutDec && !fFirst && (int)pCut->nLeaves > p->pPars->nLutDecSize ) continue; if ( pObj->fSpec && pCut->nLeaves == (unsigned)p->pPars->nLutSize ) continue; @@ -324,12 +349,32 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep { assert( p->pPars->fUseTtPerm == 0 ); assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 ); + pCut->Config = 0; if ( p->pPars->fUseDsd ) pCut->fUseless = If_DsdManCheckDec( p->pIfDsdMan, If_CutDsdLit(p, pCut) ); else if ( p->pPars->pFuncCell2 ) pCut->fUseless = !p->pPars->pFuncCell2( p, (word *)If_CutTruthW(p, pCut), pCut->nLeaves, NULL, NULL ); else + { + int iLeaf; + // Expose current cut context for user callbacks. + p->pCutObjCur = pObj; + p->pCutCur = pCut; + p->nCutLeavesCur = pCut->nLeaves; + for ( iLeaf = 0; iLeaf < p->nCutLeavesCur; iLeaf++ ) + { + If_Obj_t * pLeaf = If_CutLeaf( p, pCut, iLeaf ); + if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && pCut->nLeaves > 1 ) + { + If_Cut_t * pBestCut = If_ObjCutBest( pLeaf ); + assert( pBestCut != NULL ); + assert( pBestCut->fUseless == 0 ); + } + p->pCutLeavesCur[iLeaf] = pLeaf->Id; + p->pCutLeafArrCur[iLeaf] = If_ObjArrTime( pLeaf ); + } pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), Abc_MaxInt(6, pCut->nLeaves), pCut->nLeaves, p->pPars->pLutStruct ); + } p->nCutsUselessAll += pCut->fUseless; p->nCutsUseless[pCut->nLeaves] += pCut->fUseless; p->nCutsCountAll++; @@ -427,6 +472,27 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL ); else if ( p->pPars->fDsdBalance ) pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL ); + else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell ) + { + if ( pCut->nLeaves == 0 ) + { + pCut->Delay = 0.0; + pCut->fUseless = 0; + goto IfMapCutEvalDone; + } + if ( pCut->nLeaves == 1 ) + { + pLeaf = If_ManObj( p, pCut->pLeaves[0] ); + pCut->Delay = If_ObjArrTime( pLeaf ); + pCut->fUseless = 0; + goto IfMapCutEvalDone; + } + assert( pCut->fUseless || p->fCutDelayCurValid ); + assert( pCut->fUseless || pCut->Config != 0 ); + pCut->Delay = pCut->fUseless ? IF_FLOAT_LARGE : p->CutDelayCur; +IfMapCutEvalDone: + ; + } else if ( p->pPars->fUserRecLib ) pCut->Delay = If_CutDelayRecCost3( p, pCut, pObj ); else if ( p->pPars->fUserLutDec ) @@ -502,7 +568,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep if ( Mode && pObj->nRefs > 0 ) If_CutAreaRef( p, If_ObjCutBest(pObj) ); if ( If_ObjCutBest(pObj)->fUseless ) - Abc_Print( 1, "The best cut is useless.\n" ); + Abc_Print( 1, "The best cut is useless. Please increase the number of cuts used by the mapper, for example: \"&if -C 32\"\n" ); // call the user specified function for each cut if ( p->pPars->pFuncUser ) If_ObjForEachCut( pObj, pCut, i ) @@ -527,7 +593,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP If_Set_t * pCutSet; If_Obj_t * pTemp; If_Cut_t * pCutTemp, * pCut; - int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUse34Spec || p->pPars->fUserLutDec || p->pPars->fUserLut2D; + int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUse34Spec || p->pPars->fUserLutDec || p->pPars->fUserLut2D || p->pPars->fEnableCheck07; assert( pObj->pEquiv != NULL ); // prepare @@ -702,4 +768,3 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr ABC_NAMESPACE_IMPL_END - diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 216e4ce5ce..81f88fd72e 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -131,6 +131,20 @@ float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut ) } else { + if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib ) + { + int Intrinsic[IF_MAX_LUTSIZE]; + if ( pCut->nLeaves == 0 ) + return 0.0; + assert( pCut->nLeaves == 1 || pCut->Config != 0 ); + If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic ); + If_CutForEachLeaf( p, pCut, pLeaf, i ) + { + DelayCur = If_ObjCutBest(pLeaf)->Delay + (float)Intrinsic[i]; + Delay = IF_MAX( Delay, DelayCur ); + } + return Delay; + } if ( pCut->fUser ) { assert( !p->pPars->fLiftLeaves ); @@ -219,6 +233,17 @@ void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, fl } else { + if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib ) + { + int Intrinsic[IF_MAX_LUTSIZE]; + if ( pCut->nLeaves == 0 ) + return; + assert( (pObj && pObj->Id == 0) || pCut->nLeaves == 1 || pCut->Config != 0 ); + If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic ); + If_CutForEachLeaf( p, pCut, pLeaf, i ) + pLeaf->Required = IF_MIN( pLeaf->Required, ObjRequired - (float)Intrinsic[i] ); + return; + } if ( pCut->fUser ) { char Perm[IF_MAX_FUNC_LUTSIZE], * pPerm = Perm; @@ -452,7 +477,26 @@ void If_ManComputeRequired( If_Man_t * p ) return; // set the required times for the POs Tim_ManIncrementTravId( p->pManTim ); - if ( p->vCoAttrs ) + if ( p->pPars->pTimesReq ) + { + Counter = 0; + If_ManForEachCo( p, pObj, i ) + { + reqTime = p->pPars->pTimesReq[i]; + if ( If_ObjArrTime(If_ObjFanin0(pObj)) > reqTime + p->fEpsilon ) + { + reqTime = If_ObjArrTime(If_ObjFanin0(pObj)); + Counter++; + } + Tim_ManSetCoRequired( p->pManTim, i, reqTime ); + } + if ( Counter && !p->fReqTimeWarn ) + { + Abc_Print( 0, "Required times are exceeded at %d output%s. The earliest arrival times are used.\n", Counter, Counter > 1 ? "s":"" ); + p->fReqTimeWarn = 1; + } + } + else if ( p->vCoAttrs ) { assert( If_ManCoNum(p) == Vec_IntSize(p->vCoAttrs) ); If_ManForEachCo( p, pObj, i ) @@ -528,4 +572,3 @@ void If_ManComputeRequired( If_Man_t * p ) ABC_NAMESPACE_IMPL_END - diff --git a/src/map/if/ifTrace.c b/src/map/if/ifTrace.c new file mode 100644 index 0000000000..5a1c0d7924 --- /dev/null +++ b/src/map/if/ifTrace.c @@ -0,0 +1,42 @@ +/**CFile**************************************************************** + + FileName [ifTrace.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [FPGA mapping based on priority cuts.] + + Synopsis [Public stub for delay trace dumping.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - March 23, 2026.] + + Revision [$Id: ifTrace.c,v 1.00 2026/03/23 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "if.h" +#include "aig/gia/gia.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName ) +{ +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_IMPL_END diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 98bdf8c25e..f54b74eb3c 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -1031,12 +1031,14 @@ void * If_ManDeriveGiaFromCells2( void * pGia ) { Gia_Man_t * p = (Gia_Man_t *)pGia; Gia_Man_t * pNew, * pTemp; + If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib; Vec_Int_t * vCover, * vLeaves; Gia_Obj_t * pObj; unsigned char * pConfigData; int k, i, iLut, iVar; int Count = 0; assert( p->vConfigs2 != NULL ); + assert( pCellLib != NULL ); assert( Gia_ManHasMapping(p) ); // create new manager pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 ); @@ -1078,7 +1080,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia ) Truth = Abc_Tt6Stretch( Truth, 4 ); extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); Gia_ManObj(p, iLut)->Value = Kit_TruthToGia( pNew, (unsigned *)&Truth, Vec_IntSize(vLeaves), vCover, vLeaves, 1 ); - bytePos += 7; // 1 byte CellId + 4 bytes mapping + 2 bytes truth table + bytePos += pCellLib->pCellRecordSizes[CellId]; } else if ( CellId == 1 ) { @@ -1122,7 +1124,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia ) iObjLit2 = Kit_TruthToGia( pNew, (unsigned *)&Truth2, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 ); Gia_ManObj(p, iLut)->Value = iObjLit2; Vec_IntFree( vLeavesTemp ); - bytePos += 12; // 1 byte CellId + 7 bytes mapping + 4 bytes truth tables + bytePos += pCellLib->pCellRecordSizes[CellId]; } else if ( CellId == 2 ) { @@ -1177,7 +1179,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia ) iObjLit3 = Gia_ManHashMux( pNew, iSelectLit, iObjLit2, iObjLit1 ); Gia_ManObj(p, iLut)->Value = iObjLit3; Vec_IntFree( vLeavesTemp ); - bytePos += 14; // 1 byte CellId + 9 bytes mapping + 4 bytes truth tables + bytePos += pCellLib->pCellRecordSizes[CellId]; } else { @@ -1755,4 +1757,3 @@ void Ifn_NtkRead() ABC_NAMESPACE_IMPL_END - diff --git a/src/map/if/module.make b/src/map/if/module.make index 96c90cab8a..6be4f663e1 100644 --- a/src/map/if/module.make +++ b/src/map/if/module.make @@ -10,6 +10,7 @@ SRC += src/map/if/ifCom.c \ src/map/if/ifDec66.c \ src/map/if/ifDec75.c \ src/map/if/ifDecJ.c \ + src/map/if/ifTrace.c \ src/map/if/ifDelay.c \ src/map/if/ifDsd.c \ src/map/if/ifLibBox.c \ diff --git a/src/map/scl/sclLiberty.c b/src/map/scl/sclLiberty.c index 2064fde69d..06d40c84bf 100644 --- a/src/map/scl/sclLiberty.c +++ b/src/map/scl/sclLiberty.c @@ -559,14 +559,17 @@ static char * Io_LibLoadFileGz( char * pFileName, long * pnFileSize ) const int READ_BLOCK_SIZE = 100000; gzFile pFile; char * pContents; - long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE; + long amtRead, readBlock, nFileSize = READ_BLOCK_SIZE, nCapacity = READ_BLOCK_SIZE; pFile = gzopen( pFileName, "rb" ); // if pFileName doesn't end in ".gz" then this acts as a passthrough to fopen - pContents = ABC_ALLOC( char, nFileSize ); + pContents = ABC_ALLOC( char, nCapacity ); readBlock = 0; while ((amtRead = gzread(pFile, pContents + readBlock * READ_BLOCK_SIZE, READ_BLOCK_SIZE)) == READ_BLOCK_SIZE) { //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead); nFileSize += READ_BLOCK_SIZE; - pContents = ABC_REALLOC(char, pContents, nFileSize); + if ( nFileSize > nCapacity ) { + nCapacity *= 2; + pContents = ABC_REALLOC(char, pContents, nCapacity); + } ++readBlock; } //Abc_Print( 1,"%d: read %d bytes\n", readBlock, amtRead); diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c index 274dc0c0ec..59eac5a0d4 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 c766fb7f13..8626cf6bb5 100644 --- a/src/misc/tim/timTime.c +++ b/src/misc/tim/timTime.c @@ -98,6 +98,12 @@ 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 + // This led to an assertion failure in &if, so it is commented out below + //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 +255,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; @@ -264,4 +270,3 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo ) ABC_NAMESPACE_IMPL_END - diff --git a/src/opt/ufar/UfarCmd.cpp b/src/opt/ufar/UfarCmd.cpp index 37728b04d9..6ac2320ff4 100755 --- a/src/opt/ufar/UfarCmd.cpp +++ b/src/opt/ufar/UfarCmd.cpp @@ -15,8 +15,11 @@ #include #include #include +#include +#include #include "base/wlc/wlc.h" +#include "aig/gia/giaAig.h" #include "opt/ufar/UfarCmd.h" #include "opt/ufar/UfarMgr.h" #include "opt/untk/NtkNtk.h" @@ -120,6 +123,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv cout << "There is no current design.\n"; return 0; } + // Make each %ufar invocation stateless: always start from factory defaults. + ufar_manager.params = UFAR::UfarManager::Params(); OptMgr opt_mgr(argv[0]); opt_mgr.AddOpt("--norm", ufar_manager.params.fNorm ? "yes" : "no", "", "toggle using data type normalization"); @@ -137,9 +142,14 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv opt_mgr.AddOpt("--cbawb", ufar_manager.params.fCbaWb ? "yes" : "no", "", "toggle using cex-based refinement for white boxing"); opt_mgr.AddOpt("--grey", ufar_manager.params.fGrey ? "yes" : "no", "", "toggle using grey-box constraints"); opt_mgr.AddOpt("--grey2", to_string(ufar_manager.params.nGrey), "float", "specify the greyness threshold"); + opt_mgr.AddOpt("--allwb", ufar_manager.params.fAllWb ? "yes" : "no", "", "start with all operators white-boxed (no initial abstraction)"); + opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter"); + opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit"); opt_mgr.AddOpt("--dump", "none", "str", "specify file name"); + opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit"); opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name"); opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers"); + opt_mgr.AddOpt("--solver", "none", "str", "external solver command line"); opt_mgr.AddOpt("--dump_states", "none", "str", "specify the name for the states file"); opt_mgr.AddOpt("--read_states", "none", "str", "specify the name for the states file"); opt_mgr.AddOpt("--sp", ufar_manager.params.fSuper_prove ? "yes" : "no", "", "toggle using super_prove"); @@ -147,6 +157,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv opt_mgr.AddOpt("--syn", ufar_manager.params.fSyn ? "yes" : "no", "", "toggle using simple synthesis"); opt_mgr.AddOpt("--pth", ufar_manager.params.fPthread ? "yes" : "no", "", "toggle using pthreads"); opt_mgr.AddOpt("--onewb", to_string(ufar_manager.params.iOneWb), "int", "specify the mode for one-white-boxing"); + opt_mgr.AddOpt("--initallpairs", to_string(ufar_manager.params.nInitAllPairsLimit), "num", "pre-seed all compatible UIF pairs when #ops <= this limit (0=off)"); + opt_mgr.AddOpt("--initnear", to_string(ufar_manager.params.nInitNearMults), "num", "pre-seed UIF pairs among up to this many multipliers closest to output"); opt_mgr.AddOpt("--timeout", to_string(ufar_manager.params.nTimeout), "num", "specify the timeout (sec)"); opt_mgr.AddOpt("--exp", to_string(ufar_manager.params.iExp), "int", "specify the exp mode"); opt_mgr.AddOpt("--miter", "yes", "", "toggle mitering the problem"); @@ -174,6 +186,10 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv ufar_manager.params.fCbaWb ^= 1; if(opt_mgr["--grey"]) ufar_manager.params.fGrey ^= 1; + if(opt_mgr["--allwb"]) + ufar_manager.params.fAllWb ^= 1; + if(opt_mgr["--crossonly"]) + ufar_manager.params.fCrossOnly ^= 1; if(opt_mgr["--grey2"]) ufar_manager.params.nGrey = stof(opt_mgr.GetOptVal("--grey2")); if(opt_mgr["--sp"]) @@ -186,10 +202,16 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv ufar_manager.params.fPthread ^= 1; if(opt_mgr["--onewb"]) ufar_manager.params.iOneWb = stoi(opt_mgr.GetOptVal("--onewb")); + if(opt_mgr["--initallpairs"]) + ufar_manager.params.nInitAllPairsLimit = stoi(opt_mgr.GetOptVal("--initallpairs")); + if(opt_mgr["--initnear"]) + ufar_manager.params.nInitNearMults = stoi(opt_mgr.GetOptVal("--initnear")); if(opt_mgr["--exp"]) ufar_manager.params.iExp = stoi(opt_mgr.GetOptVal("--exp")); if(opt_mgr["--par"]) ufar_manager.params.parSetting = opt_mgr.GetOptVal("--par"); + if(opt_mgr["--solver"]) + ufar_manager.params.solverSetting = opt_mgr.GetOptVal("--solver"); if(opt_mgr["--sim"]) ufar_manager.params.simSetting = opt_mgr.GetOptVal("--sim"); if(opt_mgr["--dump_states"]) { @@ -216,7 +238,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv if(regex_search(option, sub_match, regex(R"(/?(\w+)\.v$)"))) ufar_manager.params.fileAbs = sub_match[1].str(); else - ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump"); + ufar_manager.params.fileAbs = opt_mgr.GetOptVal("--dump-abs"); } if(opt_mgr["--dump"]) { smatch sub_match; @@ -226,6 +248,9 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv else ufar_manager.params.fileName = opt_mgr.GetOptVal("--dump"); } + string firstAigDumpFile = ""; + if ( opt_mgr["--dump-first-aig"] ) + firstAigDumpFile = opt_mgr.GetOptVal("--dump-first-aig"); // ufar_manager.DumpParams(); LogT::prefix = "UIF_PROVE"; @@ -257,6 +282,68 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv Wlc_AbcUpdateNtk(pAbc, pNew); } + if ( opt_mgr["--crossstats"] ) + { + Wlc_Ntk_t * pCur = Wlc_AbcGetNtk(pAbc); + if ( Wlc_NtkPoNum(pCur) != 2 ) + { + cout << "CrossStats requires dual outputs before mitering.\n"; + return 0; + } + int nObjs = Wlc_NtkObjNumMax(pCur); + vector vConeL(nObjs, 0), vConeR(nObjs, 0); + auto mark_cone = [&]( int iStart, vector& vMark ) + { + if ( iStart < 0 || iStart >= nObjs ) + return; + vector stack(1, iStart); + while ( !stack.empty() ) + { + int iObj = stack.back(); + stack.pop_back(); + if ( iObj < 0 || iObj >= nObjs || vMark[iObj] ) + continue; + vMark[iObj] = 1; + Wlc_Obj_t * pObjT = Wlc_NtkObj(pCur, iObj); + // Sequential traversal: from flop output (FO) continue to corresponding flop input (FI). + if ( pObjT->Type == WLC_OBJ_FO ) + { + Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(pCur, pObjT); + stack.push_back( Wlc_ObjId(pCur, pFi) ); + } + int iFanin, k; + Wlc_ObjForEachFanin( pObjT, iFanin, k ) + stack.push_back(iFanin); + } + }; + int iRootL = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 0) ); + int iRootR = Wlc_ObjFaninId0( Wlc_NtkPo(pCur, 1) ); + mark_cone(iRootL, vConeL); + mark_cone(iRootR, vConeR); + + int nL = 0, nR = 0, nB = 0, nN = 0; + Wlc_Obj_t * pObjT; int iObj; + Wlc_NtkForEachObj( pCur, pObjT, iObj ) + { + if ( pObjT->Type != WLC_OBJ_ARI_MULTI ) + continue; + bool fL = vConeL[iObj] != 0; + bool fR = vConeR[iObj] != 0; + if ( fL && fR ) nB++; + else if ( fL ) nL++; + else if ( fR ) nR++; + else nN++; + } + cout << "UIF_PROVE : CrossStats: L=" << nL + << " R=" << nR + << " BOTH=" << nB + << " NONE=" << nN + << " TOTAL=" << (nL + nR + nB + nN) << endl; + //fflush(stdout); + //exit(1); + return 0; + } + if (opt_mgr["--under"]) { pNew = UFAR::MakeUnderApprox(Wlc_AbcGetNtk(pAbc), stoi(opt_mgr.GetOptVal("--under"))); Wlc_AbcUpdateNtk(pAbc, pNew); @@ -267,6 +354,12 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv Gia_Man_t * pGia = UFAR::BitBlast(Wlc_AbcGetNtk(pAbc)); Gia_ManPrintStats( pGia, NULL ); + if ( !firstAigDumpFile.empty() && firstAigDumpFile != "none" ) + { + Gia_AigerWriteSimple( pGia, (char *)firstAigDumpFile.c_str() ); + Gia_ManStop( pGia ); + return 0; + } Gia_ManStop( pGia ); ufar_manager.Initialize(Wlc_AbcGetNtk(pAbc), set_op_types); @@ -283,14 +376,61 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv gettimeofday(&t2, NULL); unsigned tTotal = elapsed_time_usec(t1, t2); if(opt_mgr["--profile"]) { + unsigned nCexChecks = 0, nBitBlasts = 0; + unsigned long long tBitBlastUsec = 0, tCexCheckUsec = 0; + UFAR::Ufar_GetOrigCexStats(&nCexChecks, &nBitBlasts, &tBitBlastUsec, &tCexCheckUsec); + LOG(0) << "OrigCexStats: checks = " << nCexChecks + << ", bitblasts = " << nBitBlasts + << ", blast_time = " << fixed << setprecision(4) << ((double)tBitBlastUsec / 1000000.0) + << " sec [" << (tTotal ? (100.0 * (double)tBitBlastUsec / (double)tTotal) : 0.0) << "%]" + << ", cex_check_time = " << ((double)tCexCheckUsec / 1000000.0) + << " sec [" << (tTotal ? (100.0 * (double)tCexCheckUsec / (double)tTotal) : 0.0) << "%]"; auto log_profile = [&](const string& str, abctime t) { - LOG(1) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]"; + LOG(0) << str << " time = " << fixed << setprecision(4) << setw(8) << (double)t/1000000 << " sec [" << setw(7) << (double)t/tTotal*100 << "%]"; + }; + auto pct = [&](unsigned n, unsigned d) { + return d ? 100.0 * (double)n / (double)d : 0.0; }; log_profile("BLSolver ", ufar_manager.profile.tBLSolver); log_profile("UifRefine ", ufar_manager.profile.tUifRefine); log_profile("WbRefine ", ufar_manager.profile.tWbRefine); log_profile("UifSim ", ufar_manager.profile.tUifSim); log_profile("GbRefine ", ufar_manager.profile.tGbRefine); + log_profile("CexCheck ", ufar_manager.profile.tCexCheckOrig); + { + unsigned long long tKnown = (unsigned long long)ufar_manager.profile.tBLSolver + + (unsigned long long)ufar_manager.profile.tUifRefine + + (unsigned long long)ufar_manager.profile.tWbRefine + + (unsigned long long)ufar_manager.profile.tUifSim + + (unsigned long long)ufar_manager.profile.tGbRefine + + (unsigned long long)ufar_manager.profile.tCexCheckOrig; + unsigned long long tUnaccounted = (tTotal > tKnown) ? (tTotal - tKnown) : 0; + LOG(0) << "Unaccounted time = " << fixed << setprecision(4) << setw(8) + << ((double)tUnaccounted / 1000000.0) << " sec [" << setw(7) + << (tTotal ? (double)tUnaccounted * 100.0 / (double)tTotal : 0.0) << "%]"; + } + LOG(0) << "UFAR calls: verify = " << ufar_manager.profile.nVerifyCalls + << " (sat = " << ufar_manager.profile.nSatCalls + << ", unsat = " << ufar_manager.profile.nUnsatCalls + << ", undec = " << ufar_manager.profile.nUnknownCalls << ")"; + LOG(0) << "UFAR cex : real = " << ufar_manager.profile.nRealCex + << ", spurious = " << ufar_manager.profile.nSpuriousCex + << " [" << fixed << setprecision(1) + << pct(ufar_manager.profile.nSpuriousCex, ufar_manager.profile.nSatCalls) + << "% spurious among SAT-abstraction]"; + LOG(0) << "UFAR ref : iters_uif = " << ufar_manager.profile.nIterUif + << ", iters_wb = " << ufar_manager.profile.nIterWb + << ", pairs_added = " << ufar_manager.profile.nUifPairsAdded + << ", mul_mul_pairs_added = " << ufar_manager.profile.nUifMulMulPairsAdded + << ", wb_added = " << ufar_manager.profile.nWbAdded; + LOG(0) << "UFAR size : max_pairs = " << ufar_manager.profile.nMaxUifPairs + << ", max_white_boxes = " << ufar_manager.profile.nMaxWhiteBoxes; + if ( ufar_manager.profile.nVerifyCalls ) { + LOG(0) << "UFAR avg : blsolve_call = " + << fixed << setprecision(4) + << (double)ufar_manager.profile.tBLSolver / 1000000.0 / (double)ufar_manager.profile.nVerifyCalls + << " sec/call"; + } } LOG(0) << "Time = " << setprecision(5) << ((double) (tTotal) / 1000000) << " sec"; diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp index 45487af771..b2177c275f 100755 --- a/src/opt/ufar/UfarMgr.cpp +++ b/src/opt/ufar/UfarMgr.cpp @@ -13,6 +13,7 @@ #include #include #include +#include #ifdef _WIN32 #include @@ -35,6 +36,27 @@ static inline unsigned log_level() { return LogT::loglevel; } +static unsigned s_nOrigCexChecks = 0; +static unsigned s_nOrigBitBlasts = 0; +static unsigned long long s_tOrigBitBlastUsec = 0; +static unsigned long long s_tOrigCexCheckUsec = 0; + +void Ufar_ResetOrigCexStats() +{ + s_nOrigCexChecks = 0; + s_nOrigBitBlasts = 0; + s_tOrigBitBlastUsec = 0; + s_tOrigCexCheckUsec = 0; +} + +void Ufar_GetOrigCexStats( unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec ) +{ + if ( pChecks ) *pChecks = s_nOrigCexChecks; + if ( pBitBlasts ) *pBitBlasts = s_nOrigBitBlasts; + if ( pBitBlastUsec ) *pBitBlastUsec = s_tOrigBitBlastUsec; + if ( pCexCheckUsec ) *pCexCheckUsec = s_tOrigCexCheckUsec; +} + static void split(const string &s, char delim, vector& elems) { stringstream ss(s); string item; @@ -132,7 +154,14 @@ static bool verify_cex_direct(Wlc_Ntk_t * pNtk, Abc_Cex_t * pCex) { } static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) { + timeval t1, t2, tCheck1, tCheck2; + gettimeofday(&tCheck1, NULL); + gettimeofday(&t1, NULL); Gia_Man_t * pGiaOrig = BitBlast(pOrig); + gettimeofday(&t2, NULL); + s_nOrigCexChecks++; + s_nOrigBitBlasts++; + s_tOrigBitBlastUsec += elapsed_time_usec(t1, t2); unsigned nbits_orig_pis = compute_bit_level_pi_num(pOrig); int nbits_ppis = pCex->nPis - Gia_ManPiNum(pGiaOrig); @@ -161,6 +190,9 @@ static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) { Gia_ManForEachPo( pGiaOrig, pObj, i ) { if (pObj->Value==1) { LOG(3) << "CEX is real."; + Gia_ManStop(pGiaOrig); + gettimeofday(&tCheck2, NULL); + s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2); return true; } } @@ -168,6 +200,8 @@ static bool verify_cex_on_original(Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex) { Gia_ManStop(pGiaOrig); LOG(3) << "CEX is spurious."; + gettimeofday(&tCheck2, NULL); + s_tOrigCexCheckUsec += elapsed_time_usec(tCheck1, tCheck2); return false; } @@ -949,6 +983,8 @@ UfarManager::Params::Params() : fGrey(false), nGrey(0), fNorm(true), + fAllWb(false), + fCrossOnly(false), fSuper_prove(false), fSimple(false), fSyn(false), @@ -956,21 +992,26 @@ UfarManager::Params::Params() : iOneWb(-1), iExp(-1), nConstraintLimit(65536), + nInitAllPairsLimit(0), + nInitNearMults(0), iVerbosity(0), nSeqLookBack(0), nTimeout(65536) {} -UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL) {} +UfarManager::UfarManager() : _pOrigNtk(NULL), _pAbsWithAuxPos(NULL), _fCrossReady(false) {} UfarManager::~UfarManager() { if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk); } void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set& types) { + Ufar_ResetOrigCexStats(); + LogT::loglevel = params.iVerbosity; if (_pOrigNtk) Wlc_NtkFree(_pOrigNtk); _vec_orig_names.clear(); _vec_op_ids.clear(); _vec_op_blackbox_marks.clear(); + _vec_op_side.clear(); _vec_op_greyness.clear(); _set_uif_pairs.clear(); _set_uif_sim_pairs.clear(); @@ -1001,12 +1042,211 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set& types) { } _vec_op_blackbox_marks.resize(_vec_op_ids.size(), true); + _vec_op_side.resize(_vec_op_ids.size(), 0); + _fCrossReady = false; + if ( params.fAllWb ) + std::fill( _vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false ); + + if ( params.fCrossOnly ) + { + int nObjs = Wlc_NtkObjNumMax(_pOrigNtk); + vector vConeL(nObjs, 0), vConeR(nObjs, 0); + auto mark_cone = [&]( int iStart, vector& vMark ) + { + if ( iStart < 0 || iStart >= nObjs ) + return; + vector stack(1, iStart); + while ( !stack.empty() ) + { + int iObj = stack.back(); + stack.pop_back(); + if ( iObj < 0 || iObj >= nObjs || vMark[iObj] ) + continue; + vMark[iObj] = 1; + Wlc_Obj_t * pObjT = Wlc_NtkObj(_pOrigNtk, iObj); + // Sequential traversal: from flop output (FO) continue to corresponding flop input (FI). + if ( pObjT->Type == WLC_OBJ_FO ) + { + Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT); + stack.push_back( Wlc_ObjId(_pOrigNtk, pFi) ); + } + int iFanin, k; + Wlc_ObjForEachFanin( pObjT, iFanin, k ) + stack.push_back(iFanin); + } + }; + + if ( Wlc_NtkPoNum(_pOrigNtk) == 1 ) + { + Wlc_Obj_t * pPo = Wlc_NtkPo(_pOrigNtk, 0); + int iMiter = Wlc_ObjFaninId0(pPo); + if ( iMiter >= 0 && iMiter < nObjs ) + { + Wlc_Obj_t * pMit = Wlc_NtkObj(_pOrigNtk, iMiter); + if ( Wlc_ObjFaninNum(pMit) >= 2 ) + { + int iL = Wlc_ObjFaninId0(pMit); + int iR = Wlc_ObjFaninId1(pMit); + mark_cone(iL, vConeL); + mark_cone(iR, vConeR); + _fCrossReady = true; + } + } + } + if ( _fCrossReady ) + { + int nL = 0, nR = 0, nB = 0, nN = 0; + for ( size_t iOp = 0; iOp < _vec_op_ids.size(); ++iOp ) + { + int iObj = _vec_op_ids[iOp]; + bool fL = vConeL[iObj] != 0; + bool fR = vConeR[iObj] != 0; + char Side = fL ? (fR ? 3 : 1) : (fR ? 2 : 0); + _vec_op_side[iOp] = Side; + if ( Side == 1 ) nL++; + else if ( Side == 2 ) nR++; + else if ( Side == 3 ) nB++; + else nN++; + } + LOG(1) << "CrossOnly: classified operators L=" << nL << " R=" << nR << " BOTH=" << nB << " NONE=" << nN; + } + else + LOG(1) << "CrossOnly: unable to derive LHS/RHS cones from miter; disabling cross filter."; + } + + auto seed_pairs_for_indices = [&]( const vector& vOpIdxs ) + { + auto sig = [&]( int iObj, int iFanin ) + { + int iFin = (iFanin == 0) ? Wlc_ObjFaninId0(Wlc_NtkObj(_pOrigNtk, iObj)) : Wlc_ObjFaninId1(Wlc_NtkObj(_pOrigNtk, iObj)); + Wlc_Obj_t * pFin = Wlc_NtkObj(_pOrigNtk, iFin); + return std::make_pair( Wlc_ObjRange(pFin), Wlc_ObjIsSigned(pFin) ); + }; + auto sigOut = [&]( int iObj ) + { + Wlc_Obj_t * pObj = Wlc_NtkObj(_pOrigNtk, iObj); + return std::make_pair( Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ); + }; + for ( size_t i = 0; i < vOpIdxs.size(); ++i ) + for ( size_t j = i + 1; j < vOpIdxs.size(); ++j ) + { + int idx1 = vOpIdxs[i]; + int idx2 = vOpIdxs[j]; + int iObj1 = _vec_op_ids[idx1]; + int iObj2 = _vec_op_ids[idx2]; + Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, iObj1); + Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, iObj2); + if ( pObj1->Type != pObj2->Type ) + continue; + if ( sigOut(iObj1) != sigOut(iObj2) ) + continue; + + bool fDirect = (sig(iObj1, 0) == sig(iObj2, 0)) && (sig(iObj1, 1) == sig(iObj2, 1)); + bool fSwap = (sig(iObj1, 0) == sig(iObj2, 1)) && (sig(iObj1, 1) == sig(iObj2, 0)); + if ( fDirect ) { + UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 0); + if ( _allow_uif_pair(Pair) ) + _set_uif_pairs.insert( Pair ); + } + if ( fSwap ) { + UIF_PAIR Pair(OperatorID(idx1), OperatorID(idx2), 1); + if ( _allow_uif_pair(Pair) ) + _set_uif_pairs.insert( Pair ); + } + } + }; + + if ( params.nInitNearMults > 0 ) + { + vector > vScoreIdx; // (seq distance from outputs, op-index in _vec_op_ids) + int nObjs = Wlc_NtkObjNumMax(_pOrigNtk); + vector vDist(nObjs, -1); + queue q; + Wlc_Obj_t * pPoT; int iPo; + Wlc_NtkForEachPo( _pOrigNtk, pPoT, iPo ) + { + int iRoot = Wlc_ObjFaninId0(pPoT); + if ( iRoot > 0 && iRoot < nObjs && vDist[iRoot] == -1 ) + { + vDist[iRoot] = 0; + q.push(iRoot); + } + } + while ( !q.empty() ) + { + int iObj = q.front(); + q.pop(); + Wlc_Obj_t * pObjT = Wlc_NtkObj(_pOrigNtk, iObj); + int dNext = vDist[iObj] + 1; + if ( pObjT->Type == WLC_OBJ_FO ) + { + Wlc_Obj_t * pFi = Wlc_ObjFo2Fi(_pOrigNtk, pObjT); + int iFi = Wlc_ObjId(_pOrigNtk, pFi); + if ( iFi > 0 && iFi < nObjs && (vDist[iFi] == -1 || dNext < vDist[iFi]) ) + { + vDist[iFi] = dNext; + q.push(iFi); + } + } + int iFanin, k; + Wlc_ObjForEachFanin( pObjT, iFanin, k ) + { + if ( iFanin <= 0 || iFanin >= nObjs ) + continue; + if ( vDist[iFanin] == -1 || dNext < vDist[iFanin] ) + { + vDist[iFanin] = dNext; + q.push(iFanin); + } + } + } + + for ( size_t i = 0; i < _vec_op_ids.size(); ++i ) + { + int iObj = _vec_op_ids[i]; + if ( Wlc_NtkObj(_pOrigNtk, iObj)->Type != WLC_OBJ_ARI_MULTI ) + continue; + if ( iObj <= 0 || iObj >= nObjs ) + continue; + if ( vDist[iObj] < 0 ) + continue; + vScoreIdx.push_back( { vDist[iObj], (int)i } ); + } + sort( vScoreIdx.begin(), vScoreIdx.end(), + []( const pair& a, const pair& b ) + { return a.first != b.first ? a.first < b.first : a.second < b.second; } ); + vector vSeedOps; + size_t nTake = Abc_MinInt( (int)vScoreIdx.size(), (int)params.nInitNearMults ); + vSeedOps.reserve( nTake ); + for ( size_t i = 0; i < nTake; ++i ) + vSeedOps.push_back( vScoreIdx[i].second ); + sort( vSeedOps.begin(), vSeedOps.end() ); + + size_t nBefore = _set_uif_pairs.size(); + seed_pairs_for_indices( vSeedOps ); + if ( _set_uif_pairs.size() > nBefore ) { + LOG(1) << "InitNear: pre-seeded " << (_set_uif_pairs.size() - nBefore) + << " UIF pairs among " << vSeedOps.size() << " closest multipliers (limit = " << params.nInitNearMults << ")"; + } + } + + if ( params.nInitAllPairsLimit > 0 && _vec_op_ids.size() <= params.nInitAllPairsLimit ) + { + vector vAllOps; + vAllOps.reserve( _vec_op_ids.size() ); + for ( size_t i = 0; i < _vec_op_ids.size(); ++i ) + vAllOps.push_back( (int)i ); + size_t nBefore = _set_uif_pairs.size(); + seed_pairs_for_indices( vAllOps ); + if ( _set_uif_pairs.size() > nBefore ) { + LOG(1) << "InitAllPairs: pre-seeded " << (_set_uif_pairs.size() - nBefore) + << " UIF pairs (ops = " << _vec_op_ids.size() << ", limit = " << params.nInitAllPairsLimit << ")"; + } + } _p_sim_mgr.reset(new SimUifPairFinder(_pOrigNtk, &_vec_op_ids)); _p_cex_mgr.reset(new CexUifPairFinder(_pOrigNtk, &_vec_op_ids)); - LogT::loglevel = params.iVerbosity; - struct timeval now; gettimeofday(&now, NULL); _timeout.tv_sec = now.tv_sec + params.nTimeout; @@ -1122,6 +1362,8 @@ void UfarManager::FindUifPairsUsingSim() { set set_new_pairs; for(auto& x:_set_uif_sim_pairs) { + if ( !_allow_uif_pair(x) ) + continue; auto res = _set_uif_pairs.insert(x); if(res.second) set_new_pairs.insert(x); @@ -1149,6 +1391,14 @@ void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) { } else { _p_cex_mgr->FindUifPairsBasic(cex_po_values, params.nSeqLookBack, set_found_pairs); } + if ( params.fCrossOnly && _fCrossReady ) + { + for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); ) + if ( !_allow_uif_pair(*it) ) + it = set_found_pairs.erase(it); + else + ++it; + } if(log_level() >= 3) print_pairs(set_found_pairs); if(params.fPbaUif && !set_found_pairs.empty()) { @@ -1171,6 +1421,14 @@ void UfarManager::FindUifPairsUsingCex(Abc_Cex_t * pCex, Abc_Cex_t ** ppCex) { } } + if ( params.fCrossOnly && _fCrossReady ) + { + for ( auto it = set_found_pairs.begin(); it != set_found_pairs.end(); ) + if ( !_allow_uif_pair(*it) ) + it = set_found_pairs.erase(it); + else + ++it; + } for(auto& x : set_found_pairs) _set_uif_pairs.insert(x); gettimeofday(&t2, NULL); @@ -1403,7 +1661,7 @@ int UfarManager::VerifyCurrentAbstraction(Abc_Cex_t ** ppCex) { } } */ - ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId); + ret = verify_model(pCurrent, ppCex, ¶ms.fileName, ¶ms.parSetting, params.fSyn, &_timeout, params.pFuncStop, params.RunId, ¶ms.solverSetting, (int)params.nTimeout); Wlc_NtkFree(pCurrent); gettimeofday(&t2, NULL); @@ -1447,9 +1705,14 @@ int UfarManager::PerformUIFProve(const timeval& timer) { LOG(1) << "Grey: [Total] = " << setprecision(4) << stat << " (" << _vec_op_greyness.size() << ")"; }; auto print_stat = [&]() { + unsigned nWhiteBoxes = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false); + if (profile.nMaxUifPairs < _set_uif_pairs.size()) + profile.nMaxUifPairs = _set_uif_pairs.size(); + if (profile.nMaxWhiteBoxes < nWhiteBoxes) + profile.nMaxWhiteBoxes = nWhiteBoxes; gettimeofday(&curTime, NULL); elapsedTime = elapsed_time_usec(timer, curTime)/1000000.0; - snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4lu White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false), _set_uif_pairs.size(), elapsedTime); + snprintf(buffer, sizeof(buffer), "Iteration[%2u][%3u]: %4u White boxes\t%4lu UIF constraints (time = %.4f)", n_iter_wb, n_iter_uif, nWhiteBoxes, _set_uif_pairs.size(), elapsedTime); LOG(1) << buffer << _get_profile_uf_wb(); dump_grey_stat(); if(!params.fileStatesOut.empty()) _dump_states(params.fileStatesOut); @@ -1491,18 +1754,28 @@ int UfarManager::PerformUIFProve(const timeval& timer) { Wlc_NtkFree(pCurrent); ret = 0; } else { + profile.nVerifyCalls++; ret = VerifyCurrentAbstraction(&mem.pCex); } if (ret == 0) { // SAT + profile.nSatCalls++; if ( Ufar_ShouldStop(params) ) return -1; // GetOperatorsInCex(mem.pCex); - if (verify_cex_on_original(_pOrigNtk, mem.pCex)) { + timeval tCheck1, tCheck2; + gettimeofday(&tCheck1, NULL); + bool fRealCex = verify_cex_on_original(_pOrigNtk, mem.pCex); + gettimeofday(&tCheck2, NULL); + profile.tCexCheckOrig += elapsed_time_usec(tCheck1, tCheck2); + if (fRealCex) { + profile.nRealCex++; PrintWordCEX(_pOrigNtk, mem.pCex, &_vec_orig_names); return 0; } + profile.nSpuriousCex++; unsigned n_before = _set_uif_pairs.size(); + set set_before = _set_uif_pairs; FindUifPairsUsingCex(mem.pCex, &mem.pCex2); if ( Ufar_ShouldStop(params) ) @@ -1534,17 +1807,28 @@ int UfarManager::PerformUIFProve(const timeval& timer) { } } + if (_set_uif_pairs.size() > n_before) + profile.nUifPairsAdded += (_set_uif_pairs.size() - n_before); + if (_set_uif_pairs.size() > n_before) { + for (const auto& x : _set_uif_pairs) { + if (set_before.find(x) == set_before.end() && _is_mul_mul_pair(x)) + profile.nUifMulMulPairsAdded++; + } + } ++n_iter_uif; + profile.nIterUif++; print_stat(); if(_set_uif_pairs.size() > params.nConstraintLimit) return -1; } else if (ret == 1) { // UNSAT + profile.nUnsatCalls++; //_shrink_final_abstraction(); //print_stat(); return 1; } else { + profile.nUnknownCalls++; return -1; } @@ -1552,9 +1836,14 @@ int UfarManager::PerformUIFProve(const timeval& timer) { if ( Ufar_ShouldStop(params) ) return -1; + unsigned nWhiteBoxesBefore = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false); DetermineWhiteBoxes(mem.pCex); + unsigned nWhiteBoxesAfter = count(_vec_op_blackbox_marks.begin(), _vec_op_blackbox_marks.end(), false); + if (nWhiteBoxesAfter > nWhiteBoxesBefore) + profile.nWbAdded += (nWhiteBoxesAfter - nWhiteBoxesBefore); ++n_iter_wb; + profile.nIterWb++; print_stat(); } return -1; @@ -1573,6 +1862,31 @@ void UfarManager::_massage_state_b() { } +bool UfarManager::_is_mul_mul_pair(const UIF_PAIR& x) const { + if (!_pOrigNtk) + return false; + if (x.first.idx >= _vec_op_ids.size() || x.second.idx >= _vec_op_ids.size()) + return false; + int obj1 = _vec_op_ids[x.first.idx]; + int obj2 = _vec_op_ids[x.second.idx]; + Wlc_Obj_t * pObj1 = Wlc_NtkObj(_pOrigNtk, obj1); + Wlc_Obj_t * pObj2 = Wlc_NtkObj(_pOrigNtk, obj2); + return pObj1 && pObj2 && pObj1->Type == WLC_OBJ_ARI_MULTI && pObj2->Type == WLC_OBJ_ARI_MULTI; +} + +bool UfarManager::_allow_uif_pair(const UIF_PAIR& x) const { + if ( !params.fCrossOnly || !_fCrossReady ) + return true; + if ( x.first.idx < 0 || x.second.idx < 0 ) + return false; + if ( x.first.idx >= (int)_vec_op_side.size() || x.second.idx >= (int)_vec_op_side.size() ) + return false; + char s1 = _vec_op_side[x.first.idx]; + char s2 = _vec_op_side[x.second.idx]; + return (s1 == 1 && s2 == 2) || (s1 == 2 && s2 == 1); +} + + string UfarManager::_get_profile_uf_wb() { if (log_level() <= 4) return ""; unsigned num_full_white = 0; @@ -1625,6 +1939,9 @@ void UfarManager::DumpParams() const { unsigned n_setw = 15; cout << "Parameters : " << endl; cout << " " << setw(n_setw) << left << "cexmin" << " : " << (params.fCexMin ? "yes" : "no") << endl; + cout << " " << setw(n_setw) << left << "allwb" << " : " << (params.fAllWb ? "yes" : "no") << endl; + cout << " " << setw(n_setw) << left << "crossonly" << " : " << (params.fCrossOnly ? "yes" : "no") << endl; + cout << " " << setw(n_setw) << left << "initnear" << " : " << params.nInitNearMults << endl; cout << " " << setw(n_setw) << left << "iLogLevel" << " : " << params.iVerbosity << endl; } diff --git a/src/opt/ufar/UfarMgr.h b/src/opt/ufar/UfarMgr.h index 31b91ef401..ad17d84748 100755 --- a/src/opt/ufar/UfarMgr.h +++ b/src/opt/ufar/UfarMgr.h @@ -42,6 +42,9 @@ typedef struct Gia_Man_t_ Gia_Man_t; namespace UFAR { +void Ufar_ResetOrigCexStats(); +void Ufar_GetOrigCexStats(unsigned * pChecks, unsigned * pBitBlasts, unsigned long long * pBitBlastUsec, unsigned long long * pCexCheckUsec); + using VecVecInt = std::vector >; using VecVecStr = std::vector >; using VecChar = std::vector; @@ -72,6 +75,8 @@ class UfarManager { bool fGrey; float nGrey; bool fNorm; + bool fAllWb; + bool fCrossOnly; bool fSuper_prove; bool fSimple; bool fSyn; @@ -79,23 +84,43 @@ class UfarManager { int iOneWb; int iExp; unsigned nConstraintLimit; + unsigned nInitAllPairsLimit; + unsigned nInitNearMults; unsigned iVerbosity; unsigned nSeqLookBack; unsigned nTimeout; std::string simSetting; std::string parSetting; + std::string solverSetting; std::string fileName; std::string fileAbs; std::string fileStatesOut; std::string fileStatesIn; }; struct Profile { - Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0) {} + Profile() : tBLSolver(0), tUifRefine(0), tWbRefine(0), tUifSim(0), tGbRefine(0), tCexCheckOrig(0), + nVerifyCalls(0), nSatCalls(0), nUnsatCalls(0), nUnknownCalls(0), + nRealCex(0), nSpuriousCex(0), nIterUif(0), nIterWb(0), + nUifPairsAdded(0), nUifMulMulPairsAdded(0), nWbAdded(0), nMaxUifPairs(0), nMaxWhiteBoxes(0) {} unsigned tBLSolver; unsigned tUifRefine; unsigned tWbRefine; unsigned tUifSim; unsigned tGbRefine; + unsigned tCexCheckOrig; + unsigned nVerifyCalls; + unsigned nSatCalls; + unsigned nUnsatCalls; + unsigned nUnknownCalls; + unsigned nRealCex; + unsigned nSpuriousCex; + unsigned nIterUif; + unsigned nIterWb; + unsigned nUifPairsAdded; + unsigned nUifMulMulPairsAdded; + unsigned nWbAdded; + unsigned nMaxUifPairs; + unsigned nMaxWhiteBoxes; }; UfarManager(); @@ -132,6 +157,8 @@ class UfarManager { void _perform_proof_based_grey_boxing(Abc_Cex_t * pCex); void _perform_cex_based_white_boxing(); std::string _get_profile_uf_wb(); + bool _is_mul_mul_pair(const UIF_PAIR& x) const; + bool _allow_uif_pair(const UIF_PAIR& x) const; void _massage_state_b(); void _dump_states(const std::string& file); void _read_states(const std::string& file); @@ -143,6 +170,7 @@ class UfarManager { std::vector _vec_op_ids; std::vector _vec_op_blackbox_marks; + std::vector _vec_op_side; // 0=unknown, 1=L-only, 2=R-only, 3=both std::vector > _vec_vec_op_ffs; std::vector _vec_op_greyness; @@ -156,6 +184,7 @@ class UfarManager { std::unique_ptr _p_cex_mgr; std::ostringstream _oss; + bool _fCrossReady; struct timespec _timeout; }; diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp index 9c2a1da857..b0cb5bd15d 100755 --- a/src/opt/untk/NtkNtk.cpp +++ b/src/opt/untk/NtkNtk.cpp @@ -11,12 +11,18 @@ #include #endif #include +#include +#include +#include +#include +#include #include #include #include #include #include +#include #include "opt/util/util.h" #include "opt/ufar/UfarPth.h" @@ -1250,11 +1256,77 @@ 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 (*pFuncStop)(int), int RunId) { +static inline bool is_solver_cmd_defined(const string* pSolverSetting) { + return pSolverSetting && !pSolverSetting->empty() && *pSolverSetting != "none"; +} + +static inline int run_external_solver_on_aig( Abc_Ntk_t * pAbcNtk, const string& solverCmd, int nRuntimeLimitSec ) +{ + const char * pAigFile = "file.aig"; + Io_Write( pAbcNtk, (char *)pAigFile, IO_FILE_AIGER ); + std::remove( "status.txt" ); + std::remove( "log.txt" ); + string command = solverCmd; + if ( command.find(pAigFile) == string::npos ) + command += string(" ") + pAigFile; + if ( nRuntimeLimitSec > 0 ) + command += " " + to_string(nRuntimeLimitSec); + command += " > log.txt 2>&1"; + LOG(1) << "UFAR external solver: launching command instead of PDR: " << command; + int res = system( command.c_str() ); + std::remove( pAigFile ); + return res; +} + +static inline int read_external_status_unsat_first_line() +{ + ifstream ifs("status.txt", std::ifstream::in); + if ( !ifs ) + return -1; + int firstLine = -1; + ifs >> firstLine; + if ( ifs && firstLine == 0 ) + return 1; + return -1; +} + +static inline int read_external_result_from_log_last_line() +{ + ifstream ifs("log.txt", std::ifstream::in); + if ( !ifs ) + return -1; + string line, last; + auto trim = []( string & s ) + { + while ( !s.empty() && isspace((unsigned char)s.front()) ) + s.erase( s.begin() ); + while ( !s.empty() && isspace((unsigned char)s.back()) ) + s.pop_back(); + }; + while ( getline(ifs, line) ) + { + trim(line); + if ( !line.empty() ) + last = line; + } + if ( last.empty() ) + return -1; + transform( last.begin(), last.end(), last.begin(), + []( unsigned char c ){ return (char)toupper(c); } ); + if ( last.find("UNSAT") != string::npos ) + return 1; + if ( last.find("SAT") != string::npos ) + return 0; + if ( last.find("UNKNOWN") != string::npos || last.find("UNDECIDED") != string::npos ) + return -1; + return -1; +} + +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, const string* pSolverSetting, int nUfarTimeoutSec) { if ( pFuncStop && pFuncStop(RunId) ) return -1; if ( !pParSetting || pParSetting->empty() || Wlc_NtkFfNum(pNtk) == 0 ) - return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId ); + return bit_level_solve( pNtk, ppCex, pFileName, pParSetting, fSyn, pFuncStop, RunId, pSolverSetting, nUfarTimeoutSec ); if(*ppCex) { Abc_CexFree(*ppCex); @@ -1275,7 +1347,7 @@ int verify_model(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileName, } -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) { +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, const string* pSolverSetting, int nRuntimeLimitSec) { if ( pFuncStop && pFuncStop(RunId) ) return -1; if(*ppCex) { @@ -1319,6 +1391,27 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam } } else { auto runPDR = [&](FILE * file){ + if ( is_solver_cmd_defined(pSolverSetting) ) + { + run_external_solver_on_aig( pAbcNtk, *pSolverSetting, nRuntimeLimitSec ); + int extStatus = read_external_result_from_log_last_line(); + if ( extStatus == -1 ) + extStatus = read_external_status_unsat_first_line(); + if ( extStatus == 1 ) + LOG(1) << "UFAR external solver result (UNSAT) available. Skipping PDR."; + else + LOG(1) << "UFAR external solver result not usable (log/status not UNSAT). Calling PDR."; + if ( extStatus == 1 ) + { + writeCexToFile(1, file, NULL); + return 1; + } + if ( pFuncStop && pFuncStop(RunId) ) + { + writeCexToFile(-1, file, NULL); + return -1; + } + } Pdr_Par_t PdrPars, *pPdrPars = &PdrPars; Pdr_ManSetDefaultParams(pPdrPars); pPdrPars->nConfLimit = 0; diff --git a/src/opt/untk/NtkNtk.h b/src/opt/untk/NtkNtk.h index 85d9ac9355..07b1c12f05 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::vector= 2 && val.back() == q; + if ( fClosed ) + val = val.substr(1, val.size() - 2); + else + { + val.erase(0, 1); + while ( i + 1 < argc ) + { + string next = argv[++i]; + if ( !next.empty() && next.back() == q ) + { + val += " " + next.substr(0, next.size() - 1); + fClosed = true; + break; + } + val += " " + next; + } + if ( !fClosed ) + return false; + } + } + opt._val = val; } } diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h index 1c31e7cc63..782afebdfc 100644 --- a/src/proof/abs/abs.h +++ b/src/proof/abs/abs.h @@ -74,6 +74,8 @@ struct Abs_Par_t_ char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag int fVeryVerbose; // print additional information + int RunId; // id in this run + int (*pFuncStop)(int); // callback to terminate int iFrame; // the number of frames covered int iFrameProved; // the number of frames proved int nFramesNoChange; // the number of last frames without changes @@ -174,4 +176,3 @@ ABC_NAMESPACE_HEADER_END //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - diff --git a/src/proof/abs/absDup.c b/src/proof/abs/absDup.c index 942155753a..8bd3b537a0 100644 --- a/src/proof/abs/absDup.c +++ b/src/proof/abs/absDup.c @@ -303,7 +303,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) int Counter0, Counter1; if ( p->vFlopClasses == NULL ) return; - if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegNum(p) ) + if ( Vec_IntSize(p->vFlopClasses) != Gia_ManRegBoxNum(p) ) { printf( "Gia_ManPrintFlopClasses(): The number of flop map entries differs from the number of flops.\n" ); return; @@ -312,7 +312,7 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ", Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) ); - if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) + if ( Counter0 + Counter1 < Gia_ManRegBoxNum(p) ) printf( "and there are other FF classes..." ); printf( "\n" ); } diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 75f991d3be..9f1a8a31e9 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1576,6 +1576,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ ) { int nAbsOld; + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + goto finish; // remember the timeframe p->pPars->iFrame = -1; // create new SAT solver @@ -1585,6 +1587,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) // unroll the circuit for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) { + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + goto finish; // remember current limits int nConflsBeg = sat_solver2_nconflicts(p->pSat); int nAbs = Vec_IntSize(p->vAbs); @@ -1618,6 +1622,11 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) nVarsOld = p->nSatVars; for ( c = 0; ; c++ ) { + if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) ) + { + Status = l_Undef; + goto finish; + } // consider the special case when the target literal is implied false // by implications which happened as a result of previous refinements // note that incremental UNSAT core cannot be computed because there is no learned clauses @@ -1898,4 +1907,3 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/abs/absUtil.c b/src/proof/abs/absUtil.c index 286d1091ba..d0d85ae41a 100644 --- a/src/proof/abs/absUtil.c +++ b/src/proof/abs/absUtil.c @@ -59,6 +59,8 @@ void Abs_ParSetDefaults( Abs_Par_t * p ) p->fUseRollback = 0; // use rollback to the starting number of frames p->fPropFanout = 1; // propagate fanouts during refinement p->fVerbose = 0; // verbose flag + p->RunId = -1; // id in this run + p->pFuncStop = NULL; // callback to terminate p->iFrame = -1; // the number of frames covered p->iFrameProved = -1; // the number of frames proved p->nFramesNoChangeLim = 2; // the number of frames without change to dump abstraction @@ -254,4 +256,3 @@ int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla ) ABC_NAMESPACE_IMPL_END - diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 8d4c730a18..0496b2e49b 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 273791fe46..cf8dfa7ed2 100644 --- a/src/proof/cec/cecProve.c +++ b/src/proof/cec/cecProve.c @@ -26,6 +26,7 @@ #include "proof/pdr/pdr.h" #include "proof/cec/cec.h" #include "proof/ssw/ssw.h" +#include "proof/abs/abs.h" #ifdef ABC_USE_PTHREADS @@ -64,6 +65,9 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in #define PAR_THR_MAX 8 #define PAR_ENGINE_UFAR 6 +#define PAR_ENGINE_SCORR1 7 +#define PAR_ENGINE_SCORR2 8 +#define PAR_ENGINE_GLA 9 struct Par_Share_t_ { volatile int fSolved; @@ -75,14 +79,37 @@ typedef struct Par_ThData_t_ Gia_Man_t * p; int iEngine; int fWorking; + int fStop; int nTimeOut; int Result; int fVerbose; int nTimeOutU; Wlc_Ntk_t * pWlc; Par_Share_t * pShare; + pthread_mutex_t Mutex; + pthread_cond_t Cond; } 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 volatile Par_Share_t * g_pGlaShare = 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-g"; + if ( iEngine == 4 ) return "pdr-t"; + if ( iEngine == 5 ) return "bmcg"; + if ( iEngine == PAR_ENGINE_UFAR ) return "ufar"; + if ( iEngine == PAR_ENGINE_SCORR1 ) return "scnew"; + if ( iEngine == PAR_ENGINE_SCORR2 ) return "scold"; + if ( iEngine == PAR_ENGINE_GLA ) return "gla-q"; + return "unknown"; +} static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst ) { char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec; @@ -108,6 +135,22 @@ static int Cec_SProveStopUfar( int RunId ) (void)RunId; return g_pUfarShare && g_pUfarShare->fSolved != 0; } +static int Cec_SProveStopGla( int RunId ) +{ + (void)RunId; + return g_pGlaShare && g_pGlaShare->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; @@ -146,15 +189,15 @@ 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 ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 ) { if ( fVerbose ) - printf( "Engine %d skipped because the current miter is combinational.\n", iEngine ); + printf( "Engine %d (%-5s) skipped because the current miter is combinational.\n", iEngine, Cec_SolveEngineName(iEngine) ); return -1; } //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock(); if ( fVerbose ) - printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut ); + printf( "Calling engine %d (%-5s) with timeout %d sec.\n", iEngine, Cec_SolveEngineName(iEngine), nTimeOut ); Abc_CexFreeP( &p->pCexSeq ); if ( iEngine == 0 ) { @@ -263,22 +306,43 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par g_pUfarShare = NULL; } } + else if ( iEngine == PAR_ENGINE_GLA ) + { + if ( Gia_ManPoNum(p) != 1 ) + return -1; + Abs_Par_t Pars, * pPars = &Pars; + Abs_ParSetDefaults( pPars ); + pPars->nTimeOut = nTimeOut; + pPars->fCallProver = 1; // emulate "&gla -q" + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; + pPars->RunId = 0; + pPars->pFuncStop = Cec_SProveStopGla; + g_pGlaShare = pThData ? pThData->pShare : NULL; + RetValue = Gia_ManPerformGla( p, pPars ); + g_pGlaShare = NULL; + } else assert( 0 ); //while ( Abc_Clock() < clkStop ); if ( pThData && pThData->pShare && RetValue != -1 ) Cec_SProveCallback( (void *)pThData, 1, (unsigned)RetValue ); if ( fVerbose ) { - printf( "Engine %d finished and %ssolved the problem. ", iEngine, RetValue != -1 ? " " : "not " ); + printf( "Engine %d (%-5s) finished and %ssolved the problem. ", iEngine, Cec_SolveEngineName(iEngine), RetValue != -1 ? " " : "not " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } 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 ); @@ -286,8 +350,11 @@ 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; @@ -296,6 +363,8 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) pPars->nLevelMax = 100; pPars->fVerbose = 0; pPars->fUseCSat = 1; + pPars->pFunc = (void *)Cec_ScorrStop; + pPars->pData = (void *)&Stop; return Cec_ManLSCorrespondence( p, pPars ); } @@ -313,58 +382,146 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p ) void * Cec_GiaProveWorkerThread( void * pArg ) { Par_ThData_t * pThData = (Par_ThData_t *)pArg; - volatile int * pPlace = &pThData->fWorking; + int status, Result; + status = pthread_mutex_lock( &pThData->Mutex ); + assert( status == 0 ); while ( 1 ) { - while ( *pPlace == 0 ); - assert( pThData->fWorking ); - if ( pThData->p == NULL ) + while ( !pThData->fWorking && !pThData->fStop ) { - pthread_exit( NULL ); - assert( 0 ); - return NULL; + status = pthread_cond_wait( &pThData->Cond, &pThData->Mutex ); + assert( status == 0 ); } - pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose, pThData ); + if ( pThData->fStop ) + break; + status = pthread_mutex_unlock( &pThData->Mutex ); + assert( status == 0 ); + Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose, pThData ); + status = pthread_mutex_lock( &pThData->Mutex ); + assert( status == 0 ); + pThData->Result = Result; pThData->fWorking = 0; + status = pthread_cond_broadcast( &pThData->Cond ); + assert( status == 0 ); } - assert( 0 ); + status = pthread_mutex_unlock( &pThData->Mutex ); + assert( status == 0 ); return NULL; } -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 ) +static void Cec_GiaStartThreads( Par_ThData_t * ThData, int nWorkers ) +{ + int i, status; + for ( i = 0; i < nWorkers; i++ ) + { + status = pthread_mutex_lock( &ThData[i].Mutex ); + assert( status == 0 ); + assert( !ThData[i].fStop ); + assert( !ThData[i].fWorking ); + ThData[i].fWorking = 1; + status = pthread_cond_signal( &ThData[i].Cond ); + assert( status == 0 ); + status = pthread_mutex_unlock( &ThData[i].Mutex ); + assert( status == 0 ); + } +} +static 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( nWorkers <= PAR_THR_MAX ); for ( i = 0; i < nWorkers; i++ ) { - ThData[i].p = Gia_ManDup(p); + if ( WorkerThread ) + { + ThData[i].p = Gia_ManDup( p ); + Cec_CopyGiaName( p, ThData[i].p ); + if ( fUseUif && i == nWorkers - 1 ) + ThData[i].iEngine = PAR_ENGINE_UFAR; + else if ( !fUseUif && nWorkers == 6 && i == 5 ) + ThData[i].iEngine = PAR_ENGINE_GLA; + else + ThData[i].iEngine = i; + ThData[i].fWorking = 0; + ThData[i].fStop = 0; + ThData[i].nTimeOut = nTimeOut; + ThData[i].Result = -1; + ThData[i].fVerbose = fVerbose; + ThData[i].nTimeOutU= nTimeOutU; + ThData[i].pWlc = pWlc; + ThData[i].pShare = pShare; + status = pthread_mutex_init( &ThData[i].Mutex, NULL ); + assert( status == 0 ); + status = pthread_cond_init( &ThData[i].Cond, NULL ); + assert( status == 0 ); + status = pthread_create( WorkerThread + i, NULL, Cec_GiaProveWorkerThread, (void *)(ThData + i) ); + assert( status == 0 ); + continue; + } + status = pthread_mutex_lock( &ThData[i].Mutex ); + assert( status == 0 ); + assert( !ThData[i].fStop ); + assert( !ThData[i].fWorking ); + Gia_ManStopP( &ThData[i].p ); + ThData[i].p = Gia_ManDup( p ); Cec_CopyGiaName( p, ThData[i].p ); - ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i; + if ( fUseUif && i == nWorkers - 1 ) + ThData[i].iEngine = PAR_ENGINE_UFAR; + else if ( !fUseUif && nWorkers == 6 && i == 5 ) + ThData[i].iEngine = PAR_ENGINE_GLA; + else + ThData[i].iEngine = 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 ); + status = pthread_mutex_unlock( &ThData[i].Mutex ); + assert( status == 0 ); } + Cec_GiaStartThreads( ThData, nWorkers ); +} +static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers ) +{ + int i, status; for ( i = 0; i < nWorkers; i++ ) - ThData[i].fWorking = 1; + { + status = pthread_mutex_lock( &ThData[i].Mutex ); + assert( status == 0 ); + ThData[i].fStop = 1; + status = pthread_cond_signal( &ThData[i].Cond ); + assert( status == 0 ); + status = pthread_mutex_unlock( &ThData[i].Mutex ); + assert( status == 0 ); + } + for ( i = 0; i < nWorkers; i++ ) + { + status = pthread_join( WorkerThread[i], NULL ); + assert( status == 0 ); + Gia_ManStopP( &ThData[i].p ); + status = pthread_cond_destroy( &ThData[i].Cond ); + assert( status == 0 ); + status = pthread_mutex_destroy( &ThData[i].Mutex ); + assert( status == 0 ); + } } -int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine ) +static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine ) { - int i; + int i, status, fWorking; for ( i = 0; i < nWorkers; i++ ) { - if ( RetValue == -1 && !ThData[i].fWorking && ThData[i].Result != -1 ) { + status = pthread_mutex_lock( &ThData[i].Mutex ); + assert( status == 0 ); + fWorking = ThData[i].fWorking; + if ( RetValue == -1 && !fWorking && ThData[i].Result != -1 ) + { RetValue = ThData[i].Result; *pRetEngine = ThData[i].iEngine; if ( !p->pCexSeq && ThData[i].p->pCexSeq ) p->pCexSeq = Abc_CexDup( ThData[i].p->pCexSeq, -1 ); } - if ( ThData[i].fWorking ) + status = pthread_mutex_unlock( &ThData[i].Mutex ); + assert( status == 0 ); + if ( fWorking ) i = -1; } return RetValue; @@ -376,8 +533,10 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Par_ThData_t ThData[PAR_THR_MAX]; pthread_t WorkerThread[PAR_THR_MAX]; Par_Share_t Share; - int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -2; + int nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -1; memset( &Share, 0, sizeof(Par_Share_t) ); + memset( ThData, 0, sizeof(ThData) ); + memset( WorkerThread, 0, sizeof(WorkerThread) ); Abc_CexFreeP( &p->pCexComb ); Abc_CexFreeP( &p->pCexSeq ); if ( !fSilent && fVerbose ) @@ -386,15 +545,20 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose ); fflush( stdout ); - assert( nProcs == 3 || nProcs == 5 ); + assert( nProcs >= 1 && nProcs <= 6 ); 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; + { + Share.fSolved = 1; + Share.Result = 1; + Share.iEngine = PAR_ENGINE_SCORR1; + RetValue = 1, RetEngine = PAR_ENGINE_SCORR1; + } RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); if ( RetValue == -1 ) @@ -406,15 +570,20 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in } Cec_GiaInitThreads( ThData, nWorkers, pScorr, nTimeOut2, nTimeOut3, pWlc, fUseUif, fVerbose, NULL, &Share ); - // meanwhile, perform scorr - if ( Gia_ManAndNum(pScorr) < 100000 ) + RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); + if ( RetValue == -1 && Gia_ManAndNum(pScorr) < 100000 ) { - Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr ); + // Run this reduction only when round-2 did not decide the problem. + Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr, nTimeOut3, &Share ); clkScorr2 = Abc_Clock() - clkStart; if ( Gia_ManAndNum(pScorr2) == 0 ) - RetValue = 1; - - RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine ); + { + Share.fSolved = 1; + Share.Result = 1; + Share.iEngine = PAR_ENGINE_SCORR2; + RetValue = 1, RetEngine = PAR_ENGINE_SCORR2; + } + if ( RetValue == -1 ) { if ( !fSilent && fVerbose ) { @@ -432,19 +601,17 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in Gia_ManStop( pScorr ); // stop threads - for ( i = 0; i < nWorkers; i++ ) - { - ThData[i].p = NULL; - ThData[i].fWorking = 1; - } + Cec_GiaStopThreads( ThData, WorkerThread, nWorkers ); if ( !fSilent ) { char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p); + if ( RetValue != -1 && RetEngine < 0 ) + RetEngine = PAR_ENGINE_SCORR1; printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" ); if ( RetValue == 0 ) - printf( "SATISFIABLE (solved by %d).", RetEngine ); + printf( "SATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); else if ( RetValue == 1 ) - printf( "UNSATISFIABLE (solved by %d).", RetEngine ); + printf( "UNSATISFIABLE (solved by %s).", Cec_SolveEngineName(RetEngine) ); else if ( RetValue == -1 ) printf( "UNDECIDED." ); else assert( 0 ); diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index a3a7e66f34..d8be282fad 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 1307d67c93..9add71284d 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 316b2e4d1c..a2654ca0b6 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 0068192375..11f60fdd9a 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 2687e9c1c0..ead977af33 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) ) diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 1b05c76050..e342ff350a 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -1363,6 +1363,161 @@ static void Exa3_ManPrintPerm( Exa3_Man_t * p ) } } } +static void Exa3_ManDumpVerilogName( Exa3_Man_t * p, char * pBase ) +{ + char Flags[32]; + int n = 0; + if ( p->pPars->pSymStr ) + snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr ); + else + snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr ); + if ( p->pPars->fUseIncr ) Flags[n++] = 'i'; + if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a'; + if ( p->pPars->fFewerVars ) Flags[n++] = 'o'; + if ( p->pPars->fLutCascade ) Flags[n++] = 'r'; + if ( p->pPars->fLutInFixed ) Flags[n++] = 'f'; + if ( p->pPars->fGlucose ) Flags[n++] = 'g'; + if ( p->pPars->fCadical ) Flags[n++] = 'c'; + if ( p->pPars->fKissat ) Flags[n++] = 'k'; + if ( p->pPars->fDumpBlif ) Flags[n++] = 'd'; + if ( p->pPars->fMinNodes ) Flags[n++] = 'm'; + if ( p->pPars->fUsePerm ) Flags[n++] = 'p'; + Flags[n] = '\0'; + snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags ); +} +static int Exa3_ManDumpCascadeVerilog( Exa3_Man_t * p, int fCompl ) +{ + static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" }; + int i, k, iVar; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + if ( !p->pPars->fSilent ) + printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" ); + return 0; + } + Exa3_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iSlice = iNode / 8; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + if ( p->nLutSize < 6 ) + Truth = Abc_Tt6Stretch( Truth, p->nLutSize ); + fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n", + iSlice, iSlice, pBels[iNode % 8] ); + fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode ); + for ( k = 0; k < 6; k++ ) + { + fprintf( pFile, " .I%d(", k ); + if ( k < p->nLutSize ) + { + iVar = Exa3_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + } + else + fprintf( pFile, "1'b0" ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) + printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName ); + return 1; +} +static int Exa3_ManDumpVerilog( Exa3_Man_t * p, int fCompl ) +{ + int i, k, iVar; + int nBits = 1 << p->nLutSize; + int nDigits = (nBits + 3) >> 2; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + if ( !p->pPars->fSilent ) + printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" ); + return 0; + } + Exa3_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode ); + for ( k = 0; k < p->nLutSize; k++ ) + { + fprintf( pFile, " .I%d(", k ); + iVar = Exa3_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) + printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); + return 1; +} /**Function************************************************************* Synopsis [] @@ -1713,7 +1868,13 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ) if ( !pPars->fSilent && (p->nUsed[0] || p->nUsed[1]) ) printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] ); if ( !pPars->fSilent ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); if ( iMint == -1 && pPars->fDumpBlif ) + { Exa3_ManDumpBlif( p, fCompl ); + if ( pPars->fLutCascade ) + Exa3_ManDumpCascadeVerilog( p, fCompl ); + else + Exa3_ManDumpVerilog( p, fCompl ); + } if ( pPars->pSymStr ) ABC_FREE( pPars->pTtStr ); Exa3_ManFree( p ); @@ -4344,4 +4505,3 @@ void Exa_NpnCascadeTest6() //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index ffc6946ae5..761795d967 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -1236,6 +1236,157 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl ) printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); ABC_FREE( pStr ); } +static void Exa3_ManDumpVerilogName( Exa3_Man_t * p, char * pBase ) +{ + char Flags[32]; + int n = 0; + if ( p->pPars->pSymStr ) + snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr ); + else + snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr ); + if ( p->pPars->fUseIncr ) Flags[n++] = 'i'; + if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a'; + if ( p->pPars->fFewerVars ) Flags[n++] = 'o'; + if ( p->pPars->fLutCascade ) Flags[n++] = 'r'; + if ( p->pPars->fLutInFixed ) Flags[n++] = 'f'; + if ( p->pPars->fGlucose ) Flags[n++] = 'g'; + if ( p->pPars->fCadical ) Flags[n++] = 'c'; + if ( p->pPars->fKissat ) Flags[n++] = 'k'; + if ( p->pPars->fDumpBlif ) Flags[n++] = 'd'; + if ( p->pPars->fMinNodes ) Flags[n++] = 'm'; + if ( p->pPars->fUsePerm ) Flags[n++] = 'p'; + Flags[n] = '\0'; + snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags ); +} +static int Exa3_ManDumpCascadeVerilog( Exa3_Man_t * p, int fCompl ) +{ + static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" }; + int i, k, iVar; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" ); + return 0; + } + Exa3_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iSlice = iNode / 8; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( sat_solver_var_value(p->pSat, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + if ( p->nLutSize < 6 ) + Truth = Abc_Tt6Stretch( Truth, p->nLutSize ); + fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n", + iSlice, iSlice, pBels[iNode % 8] ); + fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode ); + for ( k = 0; k < 6; k++ ) + { + fprintf( pFile, " .I%d(", k ); + if ( k < p->nLutSize ) + { + iVar = Exa3_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + } + else + fprintf( pFile, "1'b0" ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName ); + return 1; +} +static int Exa3_ManDumpVerilog( Exa3_Man_t * p, int fCompl ) +{ + int i, k, iVar; + int nBits = 1 << p->nLutSize; + int nDigits = (nBits + 3) >> 2; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" ); + return 0; + } + Exa3_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( sat_solver_var_value(p->pSat, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode ); + for ( k = 0; k < p->nLutSize; k++ ) + { + fprintf( pFile, " .I%d(", k ); + iVar = Exa3_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); + return 1; +} /**Function************************************************************* @@ -1445,7 +1596,16 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) Exa3_ManPrintSolution( p, fCompl ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); if ( iMint == -1 ) - Exa3_ManDumpBlif( p, fCompl ); + { + if ( pPars->fDumpBlif ) + { + Exa3_ManDumpBlif( p, fCompl ); + if ( pPars->fLutCascade ) + Exa3_ManDumpCascadeVerilog( p, fCompl ); + else + Exa3_ManDumpVerilog( p, fCompl ); + } + } if ( pPars->pSymStr ) ABC_FREE( pPars->pTtStr ); Exa3_ManFree( p ); @@ -1458,4 +1618,3 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ) ABC_NAMESPACE_IMPL_END - diff --git a/src/sat/bmc/bmcMaj7.c b/src/sat/bmc/bmcMaj7.c index dc36a61182..0a81756798 100644 --- a/src/sat/bmc/bmcMaj7.c +++ b/src/sat/bmc/bmcMaj7.c @@ -477,6 +477,161 @@ static void Exa7_ManPrintPerm( Exa7_Man_t * p ) } } } +static void Exa7_ManDumpVerilogName( Exa7_Man_t * p, char * pBase ) +{ + char Flags[32]; + int n = 0; + if ( p->pPars->pSymStr ) + snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr ); + else + snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr ); + if ( p->pPars->fUseIncr ) Flags[n++] = 'i'; + if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a'; + if ( p->pPars->fFewerVars ) Flags[n++] = 'o'; + if ( p->pPars->fLutCascade ) Flags[n++] = 'r'; + if ( p->pPars->fLutInFixed ) Flags[n++] = 'f'; + if ( p->pPars->fGlucose ) Flags[n++] = 'g'; + if ( p->pPars->fCadical ) Flags[n++] = 'c'; + if ( p->pPars->fKissat ) Flags[n++] = 'k'; + if ( p->pPars->fDumpBlif ) Flags[n++] = 'd'; + if ( p->pPars->fMinNodes ) Flags[n++] = 'm'; + if ( p->pPars->fUsePerm ) Flags[n++] = 'p'; + Flags[n] = '\0'; + snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags ); +} +static int Exa7_ManDumpCascadeVerilog( Exa7_Man_t * p, int fCompl ) +{ + static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" }; + int i, k, iVar; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + if ( !p->pPars->fSilent ) + printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" ); + return 0; + } + Exa7_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iSlice = iNode / 8; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( cadical_solver_get_var_value(p->pSat, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + if ( p->nLutSize < 6 ) + Truth = Abc_Tt6Stretch( Truth, p->nLutSize ); + fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n", + iSlice, iSlice, pBels[iNode % 8] ); + fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode ); + for ( k = 0; k < 6; k++ ) + { + fprintf( pFile, " .I%d(", k ); + if ( k < p->nLutSize ) + { + iVar = Exa7_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + } + else + fprintf( pFile, "1'b0" ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) + printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName ); + return 1; +} +static int Exa7_ManDumpVerilog( Exa7_Man_t * p, int fCompl ) +{ + int i, k, iVar; + int nBits = 1 << p->nLutSize; + int nDigits = (nBits + 3) >> 2; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + if ( !p->pPars->fSilent ) + printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" ); + return 0; + } + Exa7_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( cadical_solver_get_var_value(p->pSat, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode ); + for ( k = 0; k < p->nLutSize; k++ ) + { + fprintf( pFile, " .I%d(", k ); + iVar = Exa7_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) + printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); + return 1; +} /**Function************************************************************* @@ -829,7 +984,13 @@ int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars ) Exa7_ManPrintPerm( p ); printf( "\".\n" ); if ( pPars->fDumpBlif ) + { Exa7_ManDumpBlif( p, fCompl ); + if ( pPars->fLutCascade ) + Exa7_ManDumpCascadeVerilog( p, fCompl ); + else + Exa7_ManDumpVerilog( p, fCompl ); + } if ( p->pPars->fGenTruths ) { if ( p->pPars->vTruths ) Vec_WrdFreeP( &p->pPars->vTruths ); diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c index b0c5391a9a..5b65fbbbf4 100644 --- a/src/sat/bmc/bmcMaj8.c +++ b/src/sat/bmc/bmcMaj8.c @@ -485,6 +485,161 @@ static void Exa8_ManPrintPerm( Exa8_Man_t * p ) } } } +static void Exa8_ManDumpVerilogName( Exa8_Man_t * p, char * pBase ) +{ + char Flags[32]; + int n = 0; + if ( p->pPars->pSymStr ) + snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr ); + else + snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr ); + if ( p->pPars->fUseIncr ) Flags[n++] = 'i'; + if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a'; + if ( p->pPars->fFewerVars ) Flags[n++] = 'o'; + if ( p->pPars->fLutCascade ) Flags[n++] = 'r'; + if ( p->pPars->fLutInFixed ) Flags[n++] = 'f'; + if ( p->pPars->fGlucose ) Flags[n++] = 'g'; + if ( p->pPars->fCadical ) Flags[n++] = 'c'; + if ( p->pPars->fKissat ) Flags[n++] = 'k'; + if ( p->pPars->fDumpBlif ) Flags[n++] = 'd'; + if ( p->pPars->fMinNodes ) Flags[n++] = 'm'; + if ( p->pPars->fUsePerm ) Flags[n++] = 'p'; + Flags[n] = '\0'; + snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags ); +} +static int Exa8_ManDumpCascadeVerilog( Exa8_Man_t * p, int fCompl ) +{ + static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" }; + int i, k, iVar; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + if ( !p->pPars->fSilent ) + printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" ); + return 0; + } + Exa8_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iSlice = iNode / 8; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( Exa8_KissatVarValue(p, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + if ( p->nLutSize < 6 ) + Truth = Abc_Tt6Stretch( Truth, p->nLutSize ); + fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n", + iSlice, iSlice, pBels[iNode % 8] ); + fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode ); + for ( k = 0; k < 6; k++ ) + { + fprintf( pFile, " .I%d(", k ); + if ( k < p->nLutSize ) + { + iVar = Exa8_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + } + else + fprintf( pFile, "1'b0" ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) + printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName ); + return 1; +} +static int Exa8_ManDumpVerilog( Exa8_Man_t * p, int fCompl ) +{ + int i, k, iVar; + int nBits = 1 << p->nLutSize; + int nDigits = (nBits + 3) >> 2; + char pBase[128], pFileName[132], pModuleName[160]; + FILE * pFile; + if ( p->nLutSize > 6 ) + { + if ( !p->pPars->fSilent ) + printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" ); + return 0; + } + Exa8_ManDumpVerilogName( p, pBase ); + snprintf( pFileName, sizeof(pFileName), "%s.v", pBase ); + snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase ); + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + return 0; + fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() ); + fprintf( pFile, "module %s (\n", pModuleName ); + fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 ); + fprintf( pFile, " output wire y\n" ); + fprintf( pFile, ");\n" ); + for ( i = 0; i < p->nNodes - 1; i++ ) + fprintf( pFile, " wire n%d;\n", i ); + if ( p->nNodes > 1 ) + fprintf( pFile, "\n" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + int iNode = i - p->nVars; + int iVarStart = 1 + p->LutMask * iNode; + word Truth = 0; + word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1); + for ( k = 0; k < p->LutMask; k++ ) + if ( Exa8_KissatVarValue(p, iVarStart + k) ) + Truth |= ((word)1) << (k + 1); + if ( i == p->nObjs - 1 && fCompl ) + Truth = (~Truth) & Mask; + fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode ); + for ( k = 0; k < p->nLutSize; k++ ) + { + fprintf( pFile, " .I%d(", k ); + iVar = Exa8_ManFindFanin( p, i, k ); + if ( iVar < p->nVars ) + fprintf( pFile, "x[%d]", iVar ); + else + fprintf( pFile, "n%d", iVar - p->nVars ); + fprintf( pFile, "),\n" ); + } + if ( i == p->nObjs - 1 ) + fprintf( pFile, " .O(y)\n" ); + else + fprintf( pFile, " .O(n%d)\n", iNode ); + fprintf( pFile, " );\n\n" ); + } + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + if ( !p->pPars->fSilent ) + printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName ); + return 1; +} /**Function************************************************************* @@ -789,7 +944,13 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars ) Exa8_ManPrintPerm(p); printf( "\".\n" ); if ( pPars->fDumpBlif ) + { Exa8_ManDumpBlif( p, fCompl ); + if ( pPars->fLutCascade ) + Exa8_ManDumpCascadeVerilog( p, fCompl ); + else + Exa8_ManDumpVerilog( p, fCompl ); + } if ( p->pPars->fGenTruths ) { if ( p->pPars->vTruths ) Vec_WrdFreeP( &p->pPars->vTruths );