Handling opaque terminals

.github/workflows/regress-sec.yml

@@ -22,9 +22,19 @@ jobs:
         submodules: true
 
     - name: Install dependencies
+      timeout-minutes: 10
       run: |
-        sudo apt-get update
-        sudo apt-get install -y \
+        sudo apt-get \
+          -o Acquire::Retries=3 \
+          -o Acquire::http::Timeout=30 \
+          -o Acquire::https::Timeout=30 \
+          update
+        sudo apt-get \
+          -o Acquire::Retries=3 \
+          -o Acquire::http::Timeout=30 \
+          -o Acquire::https::Timeout=30 \
+          -o DPkg::Lock::Timeout=60 \
+          install -y \
           libgtest-dev cmake pkg-config libboost-dev libfl-dev \
           capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
           libboost-iostreams-dev zlib1g-dev
@@ -79,6 +89,7 @@ jobs:
       run: |
         cmake --build ${{github.workspace}}/build-sec-regress --target install --config Release
         chmod +x ${{github.workspace}}/stage/bin/kepler-formal
+        bash tools/bundle_linux_runtime_dependencies.sh "${{github.workspace}}/stage"
 
     - name: Upload SEC runtime
       uses: actions/upload-artifact@v4
@@ -90,7 +101,15 @@ jobs:
 
   run-sec-regress:
     name: ${{ matrix.flow.name }} / ${{ matrix.case.name }}
-    runs-on: ubuntu-22.04
+    # SEC_HEAVY_RUNNER may name a larger or self-hosted runner for full-depth
+    # GCD KI and MockAlu PDR jobs. Pull requests also use bounded smoke depths.
+    runs-on: >-
+      ${{
+        (
+          (matrix.flow.name == 'ki-dual-rail' && matrix.case.name == 'sky130hd_gcd') ||
+          (matrix.flow.name == 'pdr-dual-rail' && matrix.case.name == 'asap7_mock_alu')
+        ) && vars.SEC_HEAVY_RUNNER || 'ubuntu-22.04'
+      }}
     needs: build-sec-regress
     strategy:
       fail-fast: false
@@ -139,6 +158,7 @@ jobs:
           case_dir: kepler-formal-regress/sky130hd_gcd
           config: objects/sky130hd/gcd/base/4_rsz_lec_test.yml
           expectation: positive
+          ki_dual_rail_pr_max_k: 8
         - name: nangate45_black_parrot
           source: regress
           case_dir: kepler-formal-regress/nangate45_black_parrot
@@ -190,6 +210,7 @@ jobs:
           case_dir: kepler-formal-examples/nangate45_ariane136
           config: 6_final_sec_test.yml
           expectation: positive
+          pdr_dual_rail_expectation: allow-inconclusive
         - name: asap7_ethmac
           source: examples
           case_dir: kepler-formal-examples/asap7_ethmac
@@ -201,6 +222,7 @@ jobs:
           config: 6_final_sec_test.yml
           expectation: positive
           pdr_dual_rail_expectation: allow-inconclusive
+          pdr_dual_rail_pr_max_k: 2
         - name: asap7_mock_cpu
           source: examples
           case_dir: kepler-formal-examples/asap7_mock_cpu
@@ -269,13 +291,6 @@ jobs:
     steps:
     - uses: actions/checkout@v4
 
-    - name: Install runtime dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -y \
-          git python3 python3-pip capnproto libcapnp-dev libtbb-dev \
-          libboost-iostreams-dev zlib1g-dev
-
     - name: Download SEC runtime
       uses: actions/download-artifact@v4
       with:
@@ -311,6 +326,7 @@ jobs:
       env:
         CASE_GENERATOR: ${{ matrix.case.generator }}
       run: |
+        export LD_LIBRARY_PATH="${{github.workspace}}/stage/lib:${LD_LIBRARY_PATH:-}"
         python3 -m pip install \
           "${{github.workspace}}"/stage/najaeda/najaeda-*.whl
         case "${CASE_GENERATOR}" in
@@ -337,6 +353,8 @@ jobs:
         CASE_CONFIG: ${{ matrix.case.config }}
         CASE_EXPECTATION: ${{ matrix.case.expectation }}
         CASE_MAX_K: ${{ matrix.case.max_k }}
+        CASE_KI_DUAL_RAIL_PR_MAX_K: ${{ matrix.case.ki_dual_rail_pr_max_k }}
+        CASE_PDR_DUAL_RAIL_PR_MAX_K: ${{ matrix.case.pdr_dual_rail_pr_max_k }}
         CASE_PDR_DUAL_RAIL_EXPECTATION: ${{ matrix.case.pdr_dual_rail_expectation }}
         SEC_ENGINE: ${{ matrix.flow.engine }}
         SEC_ENCODING: ${{ matrix.flow.sec_encoding }}
@@ -361,6 +379,19 @@ jobs:
           expectation="${CASE_PDR_DUAL_RAIL_EXPECTATION}"
         fi
 
+        max_k="${CASE_MAX_K}"
+        if [[ "${GITHUB_EVENT_NAME}" == "pull_request" &&
+              "${SEC_ENGINE}" == "k_induction" &&
+              "${SEC_ENCODING}" == "dual_rail_steady" &&
+              -n "${CASE_KI_DUAL_RAIL_PR_MAX_K}" ]]; then
+          max_k="${CASE_KI_DUAL_RAIL_PR_MAX_K}"
+        elif [[ "${GITHUB_EVENT_NAME}" == "pull_request" &&
+                "${SEC_ENGINE}" == "pdr" &&
+                "${SEC_ENCODING}" == "dual_rail_steady" &&
+                -n "${CASE_PDR_DUAL_RAIL_PR_MAX_K}" ]]; then
+          max_k="${CASE_PDR_DUAL_RAIL_PR_MAX_K}"
+        fi
+
         args=(
           "${CASE_NAME}"
           "${{github.workspace}}/${CASE_DIR}"
@@ -371,8 +402,8 @@ jobs:
           "engine=${SEC_ENGINE}"
           "sec-encoding=${SEC_ENCODING}"
         )
-        if [[ -n "${CASE_MAX_K}" ]]; then
-          args+=("max-k=${CASE_MAX_K}")
+        if [[ -n "${max_k}" ]]; then
+          args+=("max-k=${max_k}")
         fi
 
         bash regress/run_sec_strategies_regress.sh "${args[@]}"
@@ -544,13 +575,6 @@ jobs:
     steps:
     - uses: actions/checkout@v4
 
-    - name: Install runtime dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -y \
-          git python3 python3-pip capnproto libcapnp-dev libtbb-dev \
-          libboost-iostreams-dev zlib1g-dev
-
     - name: Download SEC runtime
       uses: actions/download-artifact@v4
       with:
@@ -649,13 +673,6 @@ jobs:
     steps:
     - uses: actions/checkout@v4
 
-    - name: Install runtime dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -y \
-          git python3 python3-pip capnproto libcapnp-dev libtbb-dev \
-          libboost-iostreams-dev zlib1g-dev
-
     - name: Download SEC runtime
       uses: actions/download-artifact@v4
       with:

bazel/deps.bzl

@@ -33,7 +33,7 @@ _FLEX_VERSION = "2.6.4"
 _CADICAL_COMMIT = "7b99c07f0bcab5824a5a3ce62c7066554017f641"
 _GLUCOSE_COMMIT = "7f887abba7cf13636a5ac2d28653668a20a91b25"
 _KISSAT_COMMIT = "8af8e56f174b778aef3aa45af9f739b2a5f492c2"
-_NAJA_COMMIT = "abe47a6d0ff1c9392e08834440a5f3b50da134af"
+_NAJA_COMMIT = "c96e1b18bf6e411a9ed5273eac0d4cea1c79c73f"
 _NAJA_VERILOG_COMMIT = "5da040bb34f0e4e5bb8d67223b999a0132fb401f"
 _NAJA_IF_COMMIT = "099677d9f52c0db11b12c08d03e32543eebc7888"
 _SLANG_COMMIT = "512c327c209d3043aa98ecfd02d06a1b73fcd5fb"
@@ -156,7 +156,7 @@ def _deps_impl(_module_ctx):
     http_archive(
         name = "naja",
         url = "https://github.com/nanocoh/naja/archive/{}.tar.gz".format(_NAJA_COMMIT),
-        sha256 = "d7121316309a47f8fd39fe07efa308ca3e935c3ad8f0131443c3666a96d6bb17",
+        sha256 = "055337bc81b41cf6f10720950d99afed7c4ae7c328f42ec28d9185d392f33f13",
         strip_prefix = "naja-{}".format(_NAJA_COMMIT),
         build_file = Label("//bazel:naja.BUILD.bazel"),
         patch_args = ["-p0", "-f"],

docs/flags-spec.md

@@ -29,8 +29,6 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `--max-k <n>`, `-k <n>` | Set the SEC proof/search bound. Defaults to `32`; SEC only. |
 | `--sec-engine <k_induction\|imc\|pdr>` | Select the SEC engine. Defaults to `pdr`; SEC only. |
 | `--sec-encoding <binary\|dual_rail_steady>` | Select the SEC encoding. Defaults to `dual_rail_steady`; SEC only. |
-| `--sec-uncomputable-seq-boundary` | Abstract unsupported sequential instances as SEC boundaries. This is the default. |
-| `--no-sec-uncomputable-seq-boundary` | Fail SEC when an unsupported sequential instance is encountered. |
 | `--allow-boundary-mismatch` | Allow LEC to continue when top-level inputs or sequential-element outputs do not match by name. Without this flag, a mismatch stops the run before SAT solving. LEC only. |
 | `-verilog` | Use Verilog Format. |
 | `-naja_if` | Use naja-if format. |
@@ -57,7 +55,6 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `max_k` | integer | SEC proof/search bound. Defaults to `32`. |
 | `sec_engine` | string | `k_induction`, `imc`, or `pdr`. Defaults to `pdr`. |
 | `sec_encoding` | string | `binary` or `dual_rail_steady`. Defaults to `dual_rail_steady`. |
-| `sec_uncomputable_seq_as_boundary` | bool | Abstract unsupported sequential instances as SEC boundaries. Defaults to `true`. |
 | `allow-boundary-mismatch` | bool | Allow an LEC boundary mismatch. Defaults to `false`; ignored for SEC. |
 | `input_paths` | list | Required for normal runs. Accepts either `[design0, design1]` or `[[design0_file...], [design1_file...]]`. The nested form is for multi-file Verilog. |
 | `liberty_files` | list[string] | Liberty libraries loaded through `SNLLibertyConstructor`. |
@@ -109,7 +106,6 @@ verification: sec
 max_k: 32
 sec_engine: pdr
 sec_encoding: dual_rail_steady
-sec_uncomputable_seq_as_boundary: true
 input_paths:
   - [rtl_pkg.sv, rtl_top.sv]
   - [gate_top.v]

docs/sec-clock-handling.md

@@ -107,6 +107,9 @@ This means clock gating is modeled as state enable behavior rather than as a
 new independent clock. Clock-gate latch data that has been folded during SEC
 extraction is substituted before the clock event is classified, so common
 integrated clock-gating structures can still expose the intended enable.
+Generic latch models are not consumed as SEC state; the validated clock-gate
+rewrite and strict fallback behavior are documented in
+[sec-sequential-models.md](sec-sequential-models.md).
 
 ## Complex Clock Trees
 

docs/sec-flags-spec.md

@@ -14,6 +14,10 @@ library, logging, solver, CNF export, and LEC flags remain documented in
 SEC clock extraction and multi-clock-domain coverage handling are documented in
 [sec-clock-handling.md](sec-clock-handling.md).
 
+Sequential primitive support, generic latch opacity, and the clock-gate latch
+rewrite are documented in
+[sec-sequential-models.md](sec-sequential-models.md).
+
 Supported SEC flows:
 
 | Flow | Typical inputs |
@@ -33,7 +37,6 @@ kepler-formal -verilog \
   -k 4 \
   --sec-engine pdr \
   --sec-encoding dual_rail_steady \
-  --sec-uncomputable-seq-boundary \
   --report-skipped-pos \
   design0.v design1.v library.lib
 ```
@@ -84,7 +87,6 @@ verification: sec
 sec_engine: pdr
 sec_encoding: dual_rail_steady
 max_k: 32
-sec_uncomputable_seq_as_boundary: true
 compact_mode: true
 report_skipped_pos: true
 solver: kissat
@@ -104,8 +106,6 @@ liberty_files:
 | `-k <n>`, `--max-k <n>` | `max_k: <n>` | `32` | Non-negative integer | Sets the SEC proof/search bound. |
 | `--sec-engine <engine>` | `sec_engine: <engine>` | `pdr` | `k_induction`, `imc`, `pdr` | Selects the top-level SEC proof engine. Engine names are lowercase. |
 | `--sec-encoding <mode>` | `sec_encoding: <mode>` | `dual_rail_steady` | `binary`, `dual_rail_steady` | Selects how SEC models unknown or reset-unanchored state values. Omit the key/flag to use the dual-rail default. |
-| `--sec-uncomputable-seq-boundary` | `sec_uncomputable_seq_as_boundary: true` | `true` | boolean | Abstracts unsupported sequential instances as SEC boundaries instead of failing immediately. |
-| `--no-sec-uncomputable-seq-boundary` | `sec_uncomputable_seq_as_boundary: false` | `true` | boolean | Uses strict mode: unsupported sequential interfaces cause SEC to fail as unsupported. |
 | `--compact` | `compact_mode: true` | `false` | boolean | Enables compact SEC extraction: design 1 is extracted and released before design 2 is loaded; identical SEC inputs can reuse the extracted design 1 model. |
 | `--report-skipped-pos` | `report_skipped_pos: true` | `false` | boolean | Enables skipped-output reporting and writes SEC boundary reporting when entries exist. |
 
@@ -147,6 +147,14 @@ cross-design equivalence assumption. Internal names may still be used inside a
 single extracted design for diagnostics, state updates, and local recovery
 heuristics.
 
+Opaque internal elements always use strict per-output handling. If backward
+cone construction reaches any internal cell or pin without usable SEC
+semantics, traversal for that top-level output stops and the entire output is
+removed from the proof surface. SEC never substitutes a free, shared, or
+design-local proof symbol for that element. Other modeled outputs remain
+eligible for proof, so the result is partial when only some outputs are skipped
+and unsupported when no aligned verifiable output remains.
+
 ## Bounds And Results
 
 `max_k` is parsed as a non-negative integer.
@@ -174,7 +182,6 @@ The log always prints:
 SEC max_k: <n>
 SEC engine: <engine>
 SEC encoding: binary|dual_rail_steady
-SEC uncomputable sequentials: boundary abstraction|strict failure
 Compact mode: enabled|disabled
 Skipped PO reports: enabled|disabled
 ```
@@ -186,27 +193,24 @@ write the following files in the current working directory:
 
 | File | Producer | Contents |
 | --- | --- | --- |
-| `boundary_terms.txt` | SEC | Extracted SEC boundary surface. Includes top inputs, top outputs, opaque internal cut points, abstracted sequential state terms, abstracted sequential observed terms, and connectivity-skip annotations when present. |
+| `boundary_terms.txt` | SEC | Top-level SEC input/output surface and skip annotations when present. |
 | `skipped_no_driver_pos.txt` | shared cone builder | Outputs skipped because the relevant iso has no driver. |
 | `skipped_multi_driver_pos.txt` | shared cone builder | Outputs skipped because the relevant iso has multiple drivers. |
 | `skipped_logical_loop_pos.txt` | shared cone builder | Outputs skipped because the relevant cone contains a logical loop. |
 | `skipped_reset_unanchored_pos.txt` | SEC | Outputs skipped in binary SEC because their cones depend on reset-unanchored internal state. |
 | `skipped_multi_clock_domain_pos.txt` | SEC clock model | Outputs skipped because the observed output cone spans multiple extracted clock domains. |
+| `skipped_opaque_cells_pos.txt` | SEC | One entry per ignored top-level output whose backward cone reached an opaque internal cell or pin. Each entry names the output, cell, pin, and reason. |
 
 `boundary_terms.txt` starts with a category legend. Current categories are:
 
 | Role | Meaning |
 | --- | --- |
 | `top_input` | Original top-level input term. |
 | `top_output` | Original top-level output term. |
-| `opaque_internal_input` | Internal cut-point input that SEC could not reconstruct combinationally and did not model as sequential. |
-| `opaque_internal_output` | Internal cut-point output paired with an opaque internal boundary. |
-| `abstracted_sequential_state` | State-facing term exposed when an uncomputable sequential instance is abstracted as a SEC boundary. |
-| `abstracted_sequential_observed` | Observed-output-facing term exposed when an uncomputable sequential instance is abstracted as a SEC boundary. |
-
-Connectivity skipped outputs are also summarized in the main run log, including
-no-driver, multi-driver, logical-loop, reset-unanchored, and multi-clock-domain
-skips.
+
+Skipped outputs are also summarized in the main run log, including no-driver,
+multi-driver, logical-loop, reset-unanchored, multi-clock-domain, and opaque
+internal skips.
 
 ## Compact SEC
 

docs/sec-sequential-models.md

@@ -0,0 +1,80 @@
+# SEC Sequential Models
+
+This document describes which Naja sequential models Kepler Formal can use
+when extracting a transition system for Sequential Equivalence Checking (SEC).
+
+## Naja Model Contents
+
+A Naja sequential model records:
+
+- whether the element is a flip-flop or latch
+- the clock or enable expression in `clockedOn`
+- each state's next-state, clear, and preset expressions
+- the relationship between physical output pins and modeled state
+
+Models can come from Naja DB0 primitives, supported frontend lowering,
+explicit Python primitive descriptions, or Liberty construction. A cell can
+still lack a usable model when its sequential behavior is absent, incomplete,
+or not representable by the current constructor.
+
+## Flip-Flops
+
+SEC consumes flip-flop models when their state expressions and physical output
+mapping are valid. The clock expression is classified using the clock model
+described in [sec-clock-handling.md](sec-clock-handling.md), and the extracted
+state is used by all three SEC engines.
+
+Invalid or incomplete state fragments are opaque at output-terminal
+granularity. Other independently modeled outputs of the same instance remain
+eligible unless their own dependency cones reach an opaque terminal.
+
+## Latches
+
+A latch is level-sensitive. For an active-high latch, its behavior is:
+
+```text
+next_q = enable ? data : q
+```
+
+This is different from a flip-flop's edge-triggered update. Naja represents
+that distinction with `SequentialModel::Kind::Latch`, and its built-in
+`naja_dlatch` has such a model.
+
+Kepler SEC does not currently implement generic level-sensitive transition
+semantics. It therefore does not consume a Naja latch model as ordinary SEC
+state. A generic latch output is opaque and any requested top-level output
+whose cone reaches it is skipped.
+
+## Clock-Gate Latch Rewrite
+
+SEC has one narrow latch-specific rewrite for recognized clock-gating
+structures. This is not a general latch transition model.
+
+A candidate must have one latch-like output, one data input, and a gate input.
+If the primitive has a Naja sequential model, its kind must explicitly be
+`Latch`; a `FlipFlop` model never enters this rewrite. The gate must
+structurally trace to a pure clock carrier, and both the data and gate
+dependency cones must be fully modelable. When all checks pass, SEC
+substitutes the latch output with its data expression while reconstructing the
+clock-gate enable. The latch output is then removed from the extracted SEC
+state and is not published as an environment input.
+
+This rewrite captures the clock-gating abstraction used by SEC: the latch
+holds an enable stable around the active clock edge, while the consuming
+flip-flop remains the actual modeled state. If candidate recognition or
+dependency validation fails, the latch output remains opaque.
+
+## Opaque Outputs
+
+Opacity is strict and local to an output terminal. During backward cone
+construction, reaching an opaque internal output stops construction of that
+requested top-level output. SEC does not create a free, shared, or substitute
+symbol for the opaque value and does not compare the affected output.
+
+Unaffected top-level outputs remain eligible. The main result reports partial
+checked-output coverage, and `--report-skipped-pos` writes details to
+`skipped_opaque_cells_pos.txt`, including the top-level output, opaque cell and
+pin, and reason.
+
+The complete SEC reporting and flag behavior is documented in
+[sec-flags-spec.md](sec-flags-spec.md).

examples/xilinx/register_slice/test_config_verilog_xilinx_sec.yaml

@@ -5,7 +5,6 @@ format: verilog
 verification: sec
 sec_engine: pdr
 sec_encoding: dual_rail_steady
-sec_uncomputable_seq_as_boundary: false
 input_paths:
   - xilinx_register_slice_mapped.v
   - xilinx_register_slice_compact.v