Update naja

bazel/deps.bzl

@@ -33,10 +33,10 @@ _FLEX_VERSION = "2.6.4"
 _CADICAL_COMMIT = "7b99c07f0bcab5824a5a3ce62c7066554017f641"
 _GLUCOSE_COMMIT = "7f887abba7cf13636a5ac2d28653668a20a91b25"
 _KISSAT_COMMIT = "8af8e56f174b778aef3aa45af9f739b2a5f492c2"
-_NAJA_COMMIT = "83be8a9e9fc7683de50c22a91f7352a72b3783dd"
-_NAJA_VERILOG_COMMIT = "5da040bb34f0e4e5bb8d67223b999a0132fb401f"
+_NAJA_COMMIT = "6331960cb372ef6d332d07a42fb449d0bea01bbe"
+_NAJA_VERILOG_COMMIT = "be6544b128e229ce2aee814e795c1e49b02caf5c"
 _NAJA_IF_COMMIT = "099677d9f52c0db11b12c08d03e32543eebc7888"
-_SLANG_COMMIT = "512c327c209d3043aa98ecfd02d06a1b73fcd5fb"
+_SLANG_COMMIT = "b60d729d66b9cdeec158b800f898461a138d505e"
 _TOMLPLUSPLUS_COMMIT = "30172438cee64926dc41fdd9c11fb3ba5b2ba9de"
 
 def _deps_impl(_module_ctx):
@@ -131,7 +131,7 @@ def _deps_impl(_module_ctx):
     http_archive(
         name = "naja-verilog",
         url = "https://github.com/najaeda/naja-verilog/archive/{}.tar.gz".format(_NAJA_VERILOG_COMMIT),
-        sha256 = "8a0513378c419afc462ffd59c35c7d0362fee7787ab40ef23b2f0a360df0a9df",
+        sha256 = "f6fa913e9af19a589fe656bd503f9e1acb1fab11db8a563457513e76113bb003",
         strip_prefix = "naja-verilog-{}".format(_NAJA_VERILOG_COMMIT),
         patch_args = ["-p0", "-f"],
         patches = [Label("//bazel:naja_verilog_bazel9.patch")],
@@ -147,16 +147,16 @@ def _deps_impl(_module_ctx):
 
     http_archive(
         name = "slang",
-        url = "https://github.com/najaeda/slang/archive/{}.tar.gz".format(_SLANG_COMMIT),
-        sha256 = "144054285e246801a579e1365fe50c4d0a04a188025c8cb2bbe2355f653f2cbd",
+        url = "https://github.com/MikePopoloski/slang/archive/{}.tar.gz".format(_SLANG_COMMIT),
+        sha256 = "a9f65590ccf4ff2083b49f0f4352aac53e6458b04b2f1a65e24814aba3a05bc2",
         strip_prefix = "slang-{}".format(_SLANG_COMMIT),
         build_file = Label("//bazel:slang.BUILD.bazel"),
     )
 
     http_archive(
         name = "naja",
         url = "https://github.com/nanocoh/naja/archive/{}.tar.gz".format(_NAJA_COMMIT),
-        sha256 = "818723897f0db8e19796db9ea7b6af2175ec724253a83e977361b40b92c98f78",
+        sha256 = "29fb32c3bb91d777bfd1458b5a90858f4979bc075fd2e79fcac63cf16a97c1b2",
         strip_prefix = "naja-{}".format(_NAJA_COMMIT),
         build_file = Label("//bazel:naja.BUILD.bazel"),
         patch_args = ["-p0", "-f"],

bazel/naja_ff_scan.patch

@@ -149,3 +149,27 @@
 +load("@rules_cc//cc:cc_library.bzl", "cc_library")
 +
  # Vendored directly in this repo (not a submodule). naja only ever uses
+--- src/nl/formats/hdl/BUILD.bazel
++++ src/nl/formats/hdl/BUILD.bazel
+@@ -1,3 +1,5 @@
+ # SPDX-License-Identifier: Apache-2.0
+
++load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library")
++
+ cc_library(
+--- src/nl/formats/vhdl/BUILD.bazel
++++ src/nl/formats/vhdl/BUILD.bazel
+@@ -1,3 +1,5 @@
+ # SPDX-License-Identifier: Apache-2.0
+
++load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library")
++
+ cc_library(
+--- src/vhdl/BUILD.bazel
++++ src/vhdl/BUILD.bazel
+@@ -1,3 +1,5 @@
+ # SPDX-License-Identifier: Apache-2.0
+
++load("@kepler-formal//bazel:naja_cc_library.bzl", "cc_library")
++
+ cc_library(

bazel/naja_includes.bzl

@@ -25,11 +25,13 @@ _NAJA_QUOTE_INCLUDE_DIRS = [
     "src/nl/netlist/pnl",
     "src/nl/netlist/visual",
     "src/nl/netlist/serialization/capnp",
+    "src/nl/formats/hdl",
     "src/nl/formats/lefdef",
     "src/nl/formats/liberty",
     "src/nl/formats/systemverilog/frontend",
     "src/nl/formats/verilog/backend",
     "src/nl/formats/verilog/frontend",
+    "src/nl/formats/vhdl",
     "src/nl/python/pyloader",
     "src/optimization",
     "thirdparty/yosys-liberty/src",

ci/prepare_python_release.py

@@ -16,7 +16,7 @@
 import re
 
 
-DEVELOPMENT_REQUIREMENT = "najaeda==0.7.24.dev0"
+DEVELOPMENT_REQUIREMENT = "najaeda==0.7.26"
 PUBLISHED_REQUIREMENT = "najaeda==0.7.24"
 CMAKE_OPTION = "KEPLER_USE_PUBLISHED_NAJAEDA"
 VERSION_PATTERN = r'KEPLER_VERSION\s*\{\s*"(?P<value>[0-9]+\.[0-9]+\.[0-9]+)"'

ci/shared_naja_wheels.py

@@ -20,10 +20,11 @@
 import sys
 import tempfile
 
-PROVIDER_REQUIREMENT = (
-    "najaeda==0.7.24" if os.environ.get("KEPLER_USE_PUBLISHED_NAJAEDA") == "1"
-    else "najaeda==0.7.24.dev0"
-)
+# The development provider is built from thirdparty/naja and carries the same
+# version number as the NajaEDA release it is based on, so the version alone
+# cannot tell the two providers apart.
+USE_PUBLISHED_PROVIDER = os.environ.get("KEPLER_USE_PUBLISHED_NAJAEDA") == "1"
+PROVIDER_REQUIREMENT = "najaeda==0.7.24" if USE_PUBLISHED_PROVIDER else "najaeda==0.7.26"
 
 
 def run(*arguments: str, env: dict[str, str] | None = None) -> None:
@@ -148,7 +149,7 @@ def build_provider(project: Path) -> None:
                       "Windows": "delvewheel"}[platform.system()]
     run(sys.executable, "-m", "pip", "install", repair_package)
     destination = project / ".kepler-provider-wheels"
-    if ".dev" not in PROVIDER_REQUIREMENT:
+    if USE_PUBLISHED_PROVIDER:
         # Release consumers must link the exact distributed provider, not a
         # locally rebuilt same-version runtime with a different native build
         # identity. Download it for the isolated cibuildwheel test environment.

ci/windows_setup.ps1

@@ -24,7 +24,8 @@ Invoke-Checked (Join-Path $keplerVcpkgRoot 'bootstrap-vcpkg.bat') @('-disableMet
 Invoke-Checked (Join-Path $keplerVcpkgRoot 'vcpkg.exe') @(
     'install', '--triplet=x64-windows',
     'capnproto', 'tbb', 'zlib',
-    'boost-intrusive', 'boost-dynamic-bitset', 'boost-unordered', 'boost-regex'
+    'boost-intrusive', 'boost-dynamic-bitset', 'boost-multiprecision',
+    'boost-unordered', 'boost-regex'
 )
 
 # GitHub's Windows image includes LLVM and an MSVC SDK. The LLVM frontend is

docs/python-api.md

@@ -18,7 +18,7 @@ For local regression without wheels or publishing, use the
 packages from this checkout and tests their shared runtime.
 
 The default development build uses the matching NajaEDA shared-runtime SDK,
-version `0.7.24.dev0` in `thirdparty/naja`. Build both packages from this
+version `0.7.26` in `thirdparty/naja`. Build both packages from this
 recursive checkout in one virtual environment, with the native build
 dependencies installed:
 

docs/python-release.md

@@ -56,7 +56,7 @@ and [GitHub environment protection documentation](https://docs.github.com/en/act
 
 After the workflow is present on the repository's default branch, open
 **Actions → Python wheels → Run workflow**. Leave `publish` unchecked and
-`version` empty. These jobs use locally built NajaEDA `0.7.24.dev0` from the
+`version` empty. These jobs use locally built NajaEDA `0.7.26` from the
 pinned submodule and its shared-runtime SDK. The workflow builds, repairs,
 and tests wheels, then stores them as Actions artifacts. Use this to check a
 branch before merging.

pyproject.toml

@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 [build-system]
-requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.24.dev0"]
+requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.26"]
 build-backend = "scikit_build_core.build"
 
 [project]
@@ -11,7 +11,7 @@ description = "Native Python interface for Kepler Formal equivalence checking"
 authors = [{name = "keplertech.io", email = "contact@keplertech.io"}]
 readme = "src/python/README.rst"
 requires-python = ">=3.10"
-dependencies = ["najaeda==0.7.24.dev0"]
+dependencies = ["najaeda==0.7.26"]
 license = {file = "LICENSE.rst"}
 dynamic = ["version"]
 classifiers = [

test/python/test_python_release.py

@@ -18,11 +18,11 @@
 
 METADATA = '''# Keep unrelated metadata and commands intact.
 [build-system]
-requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.24.dev0"]
+requires = ["scikit-build-core>=0.11.3,<0.12", "najaeda==0.7.26"]
 
 [project]
 name = "kepler-formal"
-dependencies = ["najaeda==0.7.24.dev0"]
+dependencies = ["najaeda==0.7.26"]
 dynamic = ["version"]
 
 [tool.scikit-build.cmake.define]
@@ -78,7 +78,7 @@ def test_default_preparation_does_not_modify_checkout(self):
 
     def test_published_preparation_changes_only_pins_and_cmake_option(self):
         release.prepare_project(self.project, published_najaeda=True)
-        expected = METADATA.replace("najaeda==0.7.24.dev0", "najaeda==0.7.24").replace(
+        expected = METADATA.replace("najaeda==0.7.26", "najaeda==0.7.24").replace(
             'KEPLER_USE_PUBLISHED_NAJAEDA = "OFF"',
             'KEPLER_USE_PUBLISHED_NAJAEDA = "ON"')
         self.assertEqual(expected, self.metadata.read_text(encoding="utf-8"))
@@ -92,8 +92,8 @@ def test_published_preparation_adds_missing_cmake_option(self):
         self.assertEqual("0.5.0", self._validate())
 
     def test_mismatched_or_unsupported_provider_pins_do_not_modify_checkout(self):
-        for text in (METADATA.replace("najaeda==0.7.24.dev0", "najaeda==0.7.24", 1),
-                     METADATA.replace("najaeda==0.7.24.dev0", "najaeda>=0.7.24")):
+        for text in (METADATA.replace("najaeda==0.7.26", "najaeda==0.7.24", 1),
+                     METADATA.replace("najaeda==0.7.26", "najaeda>=0.7.24")):
             with self.subTest(text=text):
                 self.metadata.write_text(text, encoding="utf-8")
                 with self.assertRaisesRegex(ValueError, "supported provider"):

test/python/test_shared_wheel_packaging.py

@@ -21,7 +21,8 @@ class SharedWheelPackagingTests(unittest.TestCase):
     def test_release_uses_published_provider_instead_of_rebuilding_it(self):
         with tempfile.TemporaryDirectory() as temporary:
             root = Path(temporary)
-            with patch.object(helper, "PROVIDER_REQUIREMENT", "najaeda==1.2.3"), \
+            with patch.object(helper, "USE_PUBLISHED_PROVIDER", True), \
+                 patch.object(helper, "PROVIDER_REQUIREMENT", "najaeda==1.2.3"), \
                  patch.object(helper, "run") as run, \
                  patch.object(helper, "repair") as repair:
                 helper.build_provider(root)

test/scope/ScopeExtractionTests.cpp

@@ -60,6 +60,14 @@ static NLLibrary* createUniverseAndLibrary(NLUniverse*& outUniv) {
   return lib;
 }
 
+// Utility: create the standard library holding the top designs. Instances
+// cannot be created inside primitive designs, so tops live here while their
+// leaf models stay in the primitives library.
+static NLLibrary* createDesignsLibrary(NLLibrary* primitives) {
+  return NLLibrary::create(primitives->getDB(), NLLibrary::Type::Standard,
+                           NLName("designs"));
+}
+
 // Build a simple top design with two child instances and two outputs.
 // The function returns the top design pointer and also fills the instance
 // pointers and term pointers so tests can wire nets differently to create
@@ -79,7 +87,8 @@ struct TopDesignBundle {
   SNLScalarTerm* childB_out = nullptr;
 };
 
-static TopDesignBundle buildSimpleTop(NLLibrary* lib,
+static TopDesignBundle buildSimpleTop(NLLibrary* designs,
+                                      NLLibrary* lib,
                                       const std::string& topBaseName,
                                       const std::string& childANameBase,
                                       const std::string& childBNameBase) {
@@ -91,7 +100,8 @@ static TopDesignBundle buildSimpleTop(NLLibrary* lib,
 
   TopDesignBundle b;
   // Create top
-  b.top = SNLDesign::create(lib, SNLDesign::Type::Primitive, NLName(topName));
+  b.top =
+      SNLDesign::create(designs, SNLDesign::Type::Standard, NLName(topName));
   // two top outputs
   b.topOutA =
       SNLScalarTerm::create(b.top, SNLTerm::Direction::Output, NLName("outA"));
@@ -126,26 +136,31 @@ class ScopeExtractionUnitTests : public ::testing::Test {
   void SetUp() override {
     // create universe + library for each test
     lib_ = createUniverseAndLibrary(univ_);
+    designs_ = createDesignsLibrary(lib_);
   }
 
   void TearDown() override {
     // Clean up global singletons used by the SNL framework
     NLUniverse::get()->destroy();
     univ_ = nullptr;
     lib_ = nullptr;
+    designs_ = nullptr;
   }
 
   NLUniverse* univ_ = nullptr;
   NLLibrary* lib_ = nullptr;
+  NLLibrary* designs_ = nullptr;
 };
 
 // Test case: identical designs should not be added to designsToVerify_ at the
 // top level, and the algorithm should recurse into children (which are also
 // identical).
 TEST_F(ScopeExtractionUnitTests, IdenticalDesigns_NoVerificationNeeded) {
   // Build two top designs with identical structure (unique names internally)
-  TopDesignBundle a = buildSimpleTop(lib_, "topA", "LOGIC0", "LOGIC1");
-  TopDesignBundle b = buildSimpleTop(lib_, "topB", "LOGIC0", "LOGIC1");
+  TopDesignBundle a =
+      buildSimpleTop(designs_, lib_, "topA", "LOGIC0", "LOGIC1");
+  TopDesignBundle b =
+      buildSimpleTop(designs_, lib_, "topB", "LOGIC0", "LOGIC1");
 
   // Make the child models have deterministic truth tables so library tables
   // exist
@@ -184,15 +199,17 @@ TEST_F(ScopeExtractionUnitTests, IdenticalDesigns_NoVerificationNeeded) {
 // added
 TEST_F(ScopeExtractionUnitTests, DifferentInstanceCount_TopAddedToVerify) {
   // Build top A with two children
-  TopDesignBundle a = buildSimpleTop(lib_, "topA_diff", "LOGIC0", "LOGIC1");
+  TopDesignBundle a =
+      buildSimpleTop(designs_, lib_, "topA_diff", "LOGIC0", "LOGIC1");
 
   // Build top B with only one child (simulate different instance count)
   TopDesignBundle b;
   static unsigned localCounter = 0;
   ++localCounter;
   const std::string topBName =
       std::string("topB_diff_") + std::to_string(localCounter);
-  b.top = SNLDesign::create(lib_, SNLDesign::Type::Primitive, NLName(topBName));
+  b.top = SNLDesign::create(designs_, SNLDesign::Type::Standard,
+                            NLName(topBName));
   b.topOutA =
       SNLScalarTerm::create(b.top, SNLTerm::Direction::Output, NLName("outA"));
   // create only one child model and instance (unique name)
@@ -244,8 +261,10 @@ TEST_F(ScopeExtractionUnitTests, DifferentInstanceCount_TopAddedToVerify) {
 // the second top as well.
 TEST_F(ScopeExtractionUnitTests, SameCountDifferentChildIDs_AddedToVerify) {
   // Build two tops with same number of instances but different child model IDs
-  TopDesignBundle a = buildSimpleTop(lib_, "topA_ids", "LOGIC_A", "LOGIC_B");
-  TopDesignBundle b = buildSimpleTop(lib_, "topB_ids", "LOGIC_X", "LOGIC_Y");
+  TopDesignBundle a =
+      buildSimpleTop(designs_, lib_, "topA_ids", "LOGIC_A", "LOGIC_B");
+  TopDesignBundle b =
+      buildSimpleTop(designs_, lib_, "topB_ids", "LOGIC_X", "LOGIC_Y");
 
   // Set truth tables so nets/terms exist
   SNLDesignModeling::setTruthTable(a.childA_model, SNLTruthTable(0, 0, SNLTruthTable::fullDependencies(0)));