Conversation
NAJA_HEADER_COPTS hardcoded -iquoteexternal/+deps+naja/..., the
canonical repo name when kepler-formal is the root module. In a
downstream consumer (bazel_dep + git_override) the same repo
materializes at external/<consumer-visible-name>++deps+naja, the
-iquote paths dangle, quoted includes fall through to the transitive
system include paths, and headers resolve through two physical copies
(naja source tree + cmake-installed include dir) that #pragma once
cannot deduplicate:
src/src/nl/netlist/core/NLID.h:30:8: error: redefinition of 'NLID'
Derive the prefix from Label("@naja//:BUILD").workspace_root instead.
As the root module this expands to exactly the previous hardcoded
value (verified with bazel query --output=build: byte-identical
copts), and in a consumer it follows the repo mapping.
Root-module CI cannot see consumer-only breakage: canonical repo names differ between the root and dependency contexts, so a path spelled with the root-module name (external/+deps+naja) resolves in every root CI job and dangles for every consumer. The naja update surfaced exactly this (NLID redefinitions in downstream builds; fixed by #158). Adds .github/consumer-test — a minimal module that depends on the checkout via local_path_override, with the non-hermetic settings a real consumer needs (hermetic_cxx_runtime_enabled=False, preinstalled cmake toolchains) — and a workflow that builds @kepler-formal//src/bin:kepler-formal from it.
bazel: derive naja -iquote prefix from repo mapping
…dule pin The bazel build pins naja via _NAJA_COMMIT independently of the git submodule, and the two had diverged: the submodule carries najaeda commit af7695a1 (net-declaration assignment lowering, #156) while _NAJA_COMMIT still pointed at nanocoh/naja d2013782, which predates it. Point the bazel pin at najaeda/naja bfc5649 (release 0.7.13, the version verified in #156) — the one nanocoh-only commit in d2013782 landed upstream as najaeda/naja#402 — and bump _SLANG_COMMIT to the slang submodule pin recorded by naja at that commit.
ci: consumer smoke test — build kepler-formal as a bzlmod dependency
Release 0.7.13 (bfc5649) adds a producer check to SNLCapnP::load that rejects any naja-if snapshot whose recorded naja version and git hash don't exactly match the reader's. Tarball builds (bazel) stamp NAJA_GIT_HASH as "unknown" while git builds (cmake submodule, pip wheels) stamp a real hash, so the checked-in example/tinyrocket_naja*.if fixtures cannot satisfy both flows at >=0.7.13 and ExampleTestRunNajaIFWithScopeExtraction fails in the bazel CI. Pin to najaeda/naja@30f65197 instead: the exact commit thirdparty/naja records on main, which contains the #156 fix (af7695a1) and the "table select generic tt" commit (najaeda/naja#402), records the same slang/naja-verilog/naja-if pins as bfc5649, and predates the producer check. This also restores deps.bzl's convention that bazel pins mirror the thirdparty/ submodules. Any future bump past bfc5649 needs the producer check resolved upstream first. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
bazel: bump naja to najaeda 30f65197, matching the submodule pin
Use exact PDR obligations for concrete and strict rail equality, report outputs affected by uninitialized sequential logic, and add regression coverage.
bump naja
fix(sec): correct dual-rail verdicts and scale exact PDR Remove reduced SEC proof paths, their validation layer, size-limit knobs, and cross-design internal-state relations. Build PDR from exact F[0] and return partial or inconclusive when exact obligations exhaust their deterministic budgets. Align PDR, IMC, and k-induction dual-rail semantics: only opposite, binary-defined outputs form a counterexample. Clearly report successful results as equivalence under the steady-state abstraction. Improve exact PDR performance with reusable SAT encodings and F[0] solvers, adaptive output batching, certified invariant reuse, narrow predecessor queries, and bounded cache and memory ownership. Add regression coverage for resetless state, exact frame-zero handling, cache certification, batching, budgets, CLI result codes, and workflows. Document SEC exit codes: 0 proved, 1 partial, 2 inconclusive, and 3 counterexample. Fixes #157
…ween-designs docs: document LEC and SEC verification options
…ween-designs update readme and docs
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.