Py input

.github/workflows/regress-lec.yml

@@ -82,6 +82,22 @@ jobs:
           expect-identical \
           po-cnfs
 
+    # The same gcd netlists built by Python scripts through the Naja Python
+    # API must give the same verdict and the same CNF files. The Python
+    # interpreter leaks by design at exit, which the sanitizer must ignore.
+    - name: Run sky130hd_gcd_py
+      working-directory: ${{github.workspace}}
+      env:
+        ASAN_OPTIONS: detect_leaks=0
+      run: |
+        bash regress/run_cnf_regress.sh \
+          sky130hd_gcd_py \
+          "${{github.workspace}}/regress/sky130hd_gcd_py" \
+          "${{github.workspace}}/build/src/bin/kepler-formal" \
+          config.yaml \
+          expect-identical \
+          po-cnfs
+
     - name: Run nangate45_black_parrot
       working-directory: ${{github.workspace}}
       run: |

README.md

@@ -152,7 +152,7 @@ or runtime errors are execution failures rather than SEC verdicts.
 
 ```bash
 # Single file per design
-build/src/bin/kepler-formal <-verilog/-naja_if/-systemverilog/-sv/-sv2v/-vhdl> [options] \
+build/src/bin/kepler-formal <-verilog/-naja_if/-systemverilog/-sv/-sv2v/-vhdl/-python> [options] \
   <design1> <design2> [<library-file>...]
 
 # Multi-file Verilog
@@ -186,10 +186,12 @@ build/src/bin/kepler-formal -vhdl -v sec \
 | `-systemverilog`, `-sv` | Parse both designs as SystemVerilog. Requires SEC. |
 | `-sv2v` | Parse design 1 as SystemVerilog and design 2 as Verilog for SEC RTL-vs-gate comparison. |
 | `-vhdl` | Parse both designs as VHDL. Requires SEC. Experimental; see [VHDL support](docs/vhdl/README.md). |
+| `-python`, `-py` | Build both designs from Python scripts through the Naja Python API; see [Python design input](docs/python-design-input.md). |
 | `--design1 <file...>` | Explicit source list for design 1 in multi-file Verilog mode. |
 | `--design2 <file...>` | Explicit source list for design 2 in multi-file Verilog mode. |
 | `--verilog_design1_top <top>`, `--verilog_design2_top <top>` | Select the top module for each Verilog design. In `sv2v` mode, only design 2 is Verilog. |
 | `--vhdl_design1_top <top>`, `--vhdl_design2_top <top>` | Select the top entity for each VHDL design. |
+| `--python_design1_top <top>`, `--python_design2_top <top>` | Select the top module for each Python-built design. |
 | `-sv`, `-systemverilog` | Use SystemVerilog input mode. |
 | `--liberty <file...>`, `--lib <file...>` | Liberty library files. |
 | `--verilog_preprocessing` | Enable preprocessing for Verilog inputs. |
@@ -210,7 +212,7 @@ build/src/bin/kepler-formal --config <file.yaml>
 
 | Key | Type | Meaning |
 | --- | --- | --- |
-| `format` | string | `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, or `vhd`. Defaults to `verilog` if omitted. |
+| `format` | string | `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, `vhd`, `python`, or `py`. Defaults to `verilog` if omitted. |
 | `verification` | string | `lec` or `sec`. Defaults to `lec`. |
 | `btor2_export` | bool | Enable BTOR2 export before solving; SEC only. Defaults to `false`. |
 | `btor2_export_path` | string | BTOR2 destination; defaults to `miter.btor2` when enabled. Requires `btor2_export: true`. |

docs/flags-spec.md

@@ -18,6 +18,7 @@ The SEC-specific flag surface is documented separately in
 | `sec` | RTL-level sequential equivalence checking | RTL Verilog/SystemVerilog sources, including SystemVerilog flists with explicit tops. |
 | `sec` | SystemVerilog-to-Verilog RTL-vs-gate checking (`sv2v`) | SystemVerilog design 1 and Verilog design 2, plus Liberty/Python primitive libraries as needed. |
 | `sec` | VHDL RTL-level sequential equivalence checking (`vhdl`) | VHDL sources for both designs, in compile order. Experimental; see [VHDL support](vhdl/README.md). |
+| `lec`, `sec` | Designs built by Python scripts (`python`) | One or more scripts per design that create the design with the Naja Python API, plus Liberty/Python primitive libraries. See [Python design input](python-design-input.md). |
 
 LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 `verification: sec` in YAML.
@@ -43,6 +44,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `-systemverilog`, `-sv` | Use SystemVerilog format for both designs. Requires SEC verification. |
 | `-sv2v` | Use mixed SystemVerilog-to-Verilog format for SEC RTL-vs-gate comparison: design 1 is parsed as SystemVerilog, design 2 is parsed as Verilog. |
 | `-vhdl` | Use VHDL format for both designs. Requires SEC verification. |
+| `-python`, `-py` | Build both designs from Python scripts through the Naja Python API. |
 | `--help`, `-h` | Print usage and exit. |
 | `--version`, `-V` | Print the embedded Kepler Formal and Naja versions and Git hashes to stdout and exit successfully. Use as a standalone option. |
 | `--config <file>`, `-c <file>` | Load a YAML config file. Config mode cannot be combined with other command-line options. |
@@ -54,14 +56,15 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `--sv_design1_top <top>`, `--sv_design2_top <top>` | Per-design SystemVerilog top modules. Only design 1 is valid in `sv2v` mode. |
 | `--verilog_design1_top <top>`, `--verilog_design2_top <top>` | Per-design Verilog top modules. Only design 2 is valid in `sv2v` mode. |
 | `--vhdl_design1_top <top>`, `--vhdl_design2_top <top>` | Per-design VHDL top entities. Only valid in `vhdl` mode. |
+| `--python_design1_top <top>`, `--python_design2_top <top>` | Per-design top modules of Python-built designs. Only valid in `python` mode. |
 | `--compact` | Reduce peak memory. In SEC, extract and release design 1 before loading design 2. |
 | `--report-skipped-pos` | Emit skipped-PO reports in the current working directory. |
 
 ## YAML config flags
 
 | Key | Type | Meaning |
 | --- | --- | --- |
-| `format` | string | Input format: `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, or `vhd`. If omitted, the implementation defaults to `verilog`. |
+| `format` | string | Input format: `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, `vhd`, `python`, or `py`. If omitted, the implementation defaults to `verilog`. |
 | `verification` | string | `lec` or `sec`. Defaults to `lec`. |
 | `max_k` | integer | SEC proof/search bound. Defaults to `32`. |
 | `sec_engine` | string | `k_induction`, `imc`, or `pdr`. Defaults to `pdr`. |
@@ -92,6 +95,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `sv_design1_top`, `sv_design2_top` | string | Per-design SystemVerilog top modules. Only design 1 is valid in `sv2v` mode. |
 | `verilog_design1_top`, `verilog_design2_top` | string | Per-design Verilog top modules. Only design 2 is valid in `sv2v` mode. |
 | `vhdl_design1_top`, `vhdl_design2_top` | string | Per-design VHDL top entities. Only valid in `vhdl` mode. |
+| `python_design1_top`, `python_design2_top` | string | Per-design top modules of Python-built designs. Only valid in `python` mode. |
 | `solver` | string | SAT solver selection: `kissat`, `glucose`, or `cadical`. Defaults to `kissat`. |
 
 Example:

docs/python-design-input.md

@@ -0,0 +1,87 @@
+# Python Design Input
+
+A design can be given as a Python script instead of a netlist file. The script
+builds the design with the Naja Python API, the same API that
+[Python primitive files](python-primitives.md) use for technology cells. The
+mode is for netlists produced or transformed by a program: every module,
+instance, net and connection is created by calling the API.
+
+## Usage
+
+CLI flag: `-python` (or `-py`). YAML: `format: python` (or `py`). The mode
+works for LEC and SEC.
+
+```bash
+build/src/bin/kepler-formal -python -v sec \
+  --design1 <script...> --design2 <script...> \
+  --liberty <cells.lib> \
+  [--python_design1_top <top>] [--python_design2_top <top>]
+```
+
+```yaml
+format: python
+verification: lec
+input_paths:
+  - [design1/cells.py, design1/top.py]
+  - [design2/top.py]
+py_tech_files:
+  - ./my_primitives.py
+python_design1_top: top
+python_design2_top: top
+```
+
+## Script contract
+
+Each script defines `constructLibrary(lib)`. Kepler-formal calls it with the
+design library of one side, after the technology primitives are loaded. The
+scripts of a design run in the listed order against the same library, so a
+design may be split over several files.
+
+```python
+import naja
+
+
+def constructLibrary(lib):
+    inv = primitive(lib, "INV")
+    top = naja.SNLDesign.create(lib, "top")
+    a = naja.SNLScalarTerm.create(top, naja.SNLTerm.Direction.Input, "a")
+    y = naja.SNLScalarTerm.create(top, naja.SNLTerm.Direction.Output, "y")
+    net_a = naja.SNLScalarNet.create(top, "a")
+    net_y = naja.SNLScalarNet.create(top, "y")
+    a.setNet(net_a)
+    y.setNet(net_y)
+    gate = naja.SNLInstance.create(top, inv, "u_inv")
+    gate.getInstTerm(inv.getScalarTerm("A")).setNet(net_a)
+    gate.getInstTerm(inv.getScalarTerm("Y")).setNet(net_y)
+```
+
+Primitive cells come from `py_tech_files` or `--liberty`, as in every other
+mode. They live in the primitive libraries of the design's database. A Liberty
+library keeps the name declared in the file, so look a cell up in every
+primitive library rather than by library name:
+
+```python
+def primitive(lib, name):
+    for primitives in lib.getDB().getPrimitiveLibraries():
+        model = primitives.getSNLDesign(name)
+        if model is not None:
+            return model
+    raise RuntimeError("primitive %s was not loaded" % name)
+```
+
+## Top selection
+
+`python_design1_top` and `python_design2_top` name the top module of each
+design. Without them the top is the module that no other module instantiates.
+When several modules qualify, name the top explicitly; the run stops with
+`No top design was found` otherwise. A named top that the script did not
+create stops the run with an error.
+
+## Notes
+
+- The script's `print` output is only shown when written to `sys.stderr` or
+  flushed; a run that stops on an error does not flush Python's `stdout`.
+- `naja.so` must be importable, as for Python primitive files; see
+  [How `naja.so` is found](python-primitives.md#how-najaso-is-found).
+- The in-process `kepler_formal` Python API does not accept this format. It
+  borrows live NajaEDA designs instead; see [Python API](python-api.md).

regress/sky130hd_gcd_py/config.yaml

@@ -0,0 +1,13 @@
+# Copyright 2026 keplertech.io
+# SPDX-License-Identifier: Apache-2.0
+# The sky130hd_gcd LEC regression with both netlists given as Python scripts
+# (format: python). The scripts were generated from the Verilog netlists of
+# kepler-formal-regress/sky130hd_gcd by verilog_to_naja_py.py, so the loaded
+# designs, the verdict and the exported CNF are the same as for the Verilog
+# inputs; the golden archives are those of sky130hd_gcd.
+format: python
+input_paths:
+  - ./gcd_before.py
+  - ./gcd_after.py
+liberty_files:
+  - ../../kepler-formal-regress/sky130hd_gcd/sky130_fd_sc_hd__tt_025C_1v80.lib