Update

README.md

@@ -155,7 +155,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> [options] \
+build/src/bin/kepler-formal <-verilog/-naja_if/-systemverilog/-sv/-sv2v/-vhdl> [options] \
   <design1> <design2> [<library-file>...]
 
 # Multi-file Verilog
@@ -168,6 +168,11 @@ build/src/bin/kepler-formal -sv -v sec \
   --sv_design1_flist <file> --sv_design1_top <top> \
   --sv_design2_flist <file> --sv_design2_top <top> \
   [--liberty <library-file>...]
+
+# VHDL SEC, files in compile order with the top-level unit last
+build/src/bin/kepler-formal -vhdl -v sec \
+  --design1 <file...> --design2 <file...> \
+  [--vhdl_design1_top <top>] [--vhdl_design2_top <top>]
 ```
 
 | Flag | Meaning |
@@ -183,9 +188,11 @@ build/src/bin/kepler-formal -sv -v sec \
 | `-naja_if` | Parse both designs as Naja IF. |
 | `-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). |
 | `--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. |
 | `-sv`, `-systemverilog` | Use SystemVerilog input mode. |
 | `--liberty <file...>`, `--lib <file...>` | Liberty library files. |
 | `--verilog_preprocessing` | Enable preprocessing for Verilog inputs. |
@@ -206,14 +213,15 @@ build/src/bin/kepler-formal --config <file.yaml>
 
 | Key | Type | Meaning |
 | --- | --- | --- |
-| `format` | string | `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, or `sv2v`. Defaults to `verilog` if omitted. |
+| `format` | string | `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, or `vhd`. 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`. |
 | `dump_only` | bool | Stop after export without solving. Defaults to `false`; requires `btor2_export: true`. |
 | `allow-boundary-mismatch` | bool | Allow an LEC boundary mismatch. Defaults to `false`; ignored for SEC. |
 | `input_paths` | list | Required. Either `[design0, design1]` or `[[design0_file...], [design1_file...]]`. The nested form is for multi-file Verilog. |
 | `verilog_design1_top`, `verilog_design2_top` | string | Select the top module for each Verilog design. In `sv2v` mode, only `verilog_design2_top` is valid. |
+| `vhdl_design1_top`, `vhdl_design2_top` | string | Select the top entity for each VHDL design. Only valid with `format: vhdl`. |
 | `liberty_files` | list[string] | Liberty libraries loaded through `SNLLibertyConstructor`. |
 | `py_tech_files` | list[string] | Python primitive loaders loaded through `SNLPyLoader`. |
 | `verilog_preprocessing` | bool | Enable preprocessing for Verilog inputs. |

bazel/naja.BUILD.bazel

@@ -10,6 +10,7 @@ cc_library(
         "//src/nl/formats/liberty:naja_snl_liberty",
         "//src/nl/formats/systemverilog:naja_snl_systemverilog",
         "//src/nl/formats/verilog:naja_snl_verilog",
+        "//src/nl/formats/vhdl:naja_snl_vhdl",
         "//src/nl/netlist:naja_nl",
         "//src/nl/netlist:naja_snl_visual",
         "//src/nl/netlist/serialization/capnp:naja_nl_dump",

docs/flags-spec.md

@@ -17,6 +17,7 @@ The SEC-specific flag surface is documented separately in
 | `sec` | Gate-level sequential equivalence checking | Sequential Verilog/SystemVerilog netlists plus Liberty/Python primitive libraries as needed. |
 | `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 is the default. Select SEC with `-v sec`, `--verification sec`, or
 `verification: sec` in YAML.
@@ -41,6 +42,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `-naja_if` | Use naja-if format. |
 | `-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. |
 | `--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. |
@@ -51,14 +53,15 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `--sv_design1_flist <file>`, `--sv_design2_flist <file>` | Per-design SystemVerilog file lists. Only design 1 is valid in `sv2v` mode. |
 | `--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. |
 | `--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`, or `sv2v`. If omitted, the implementation defaults to `verilog`. |
+| `format` | string | Input format: `verilog`, `v`, `naja_if`, `systemverilog`, `sv`, `sv2v`, `vhdl`, or `vhd`. 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`. |
@@ -88,6 +91,7 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `sv_design1_flist`, `sv_design2_flist` | string | Per-design SystemVerilog file lists. Only design 1 is valid in `sv2v` mode. |
 | `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. |
 | `solver` | string | SAT solver selection: `kissat`, `glucose`, or `cadical`. Defaults to `kissat`. |
 
 Example:

docs/vhdl/README.md

@@ -0,0 +1,74 @@
+# VHDL Support
+
+This document tracks the VHDL flow in `kepler-formal`.
+
+Status:
+
+- experimental: the VHDL frontend in Naja is in beta and accepts a restricted
+  RTL subset
+- supported for RTL-level SEC, with both designs given as VHDL
+- the `vhdl` input mode requires SEC verification
+
+## Usage
+
+CLI flag: `-vhdl`. YAML: `format: vhdl` (or `vhd`).
+
+```bash
+# Single file per design
+build/src/bin/kepler-formal -vhdl -v sec <design1.vhd> <design2.vhd>
+
+# Multi-file VHDL designs
+build/src/bin/kepler-formal -vhdl -v sec \
+  --design1 <file...> --design2 <file...> \
+  [--vhdl_design1_top <top>] [--vhdl_design2_top <top>]
+```
+
+```yaml
+format: vhdl
+verification: sec
+vhdl_design1_top: top
+vhdl_design2_top: top
+input_paths:
+  - [design1/pkg.vhd, design1/leaf.vhd, design1/top.vhd]
+  - [design2/top.vhd]
+```
+
+## File order
+
+Files are loaded one at a time, in the order given, and each file can use the
+units of the files before it. List them in compile order: packages and
+instantiated entities first, the top-level unit last. A file that instantiates
+an entity from a later file is rejected with a `missing entity` error.
+
+## Top selection
+
+`vhdl_design1_top` and `vhdl_design2_top` name the top entity of each design.
+The top is elaborated after the last file is loaded, so it may be declared in
+any of the files.
+
+Without a top option, the top is the design built from the last file that
+produces one; package-only files produce none. When that file declares several
+entities, the top is the one no other entity instantiates. Name the top
+explicitly whenever the last file is not the top-level unit.
+
+## Supported language subset
+
+Naja lowers VHDL to the same primitives as its SystemVerilog frontend, as
+two-state hardware. The subset covers `bit`, `bit_vector` and imported
+`std_logic` types, concurrent and conditional assignments, positive-edge
+processes with synchronous reset and enable, constrained arrays with static
+indexing, and direct entity instantiation. See
+`thirdparty/naja/src/vhdl/README.md` for the current limits.
+
+A construct outside the subset stops the run with an error that names the file
+and line. It is never approximated.
+
+## Notes
+
+- Warnings from the VHDL frontend are printed on the console. No separate
+  diagnostics report is written.
+- Registers without a reset bootstrap need the default `dual_rail_steady`
+  encoding. With `sec_encoding: binary`, give a reset bootstrap through
+  `sec_reset`; see [SEC reset bootstrap](../sec-reset-bootstrap.md).
+- Mixed comparisons, such as VHDL against Verilog or SystemVerilog, are not
+  available.

src/bin/CMakeLists.txt

@@ -38,6 +38,7 @@ set(KEPLER_FORMAL_DRIVER_LIBRARIES
     naja_snl_liberty
     naja_snl_systemverilog
     naja_snl_verilog
+    naja_snl_vhdl
     kissat
     cadical
     formal_strategies