update readme and docs

README.md

@@ -27,6 +27,7 @@ This project is supported and funded by NLNet through the [NGI0 Entrust](https:/
 | Gate-level LEC | Post-synthesis or implementation netlists plus Liberty libraries | `lec` |
 | Gate-level SEC | Sequential gate-level netlists plus Liberty libraries | `sec` |
 | RTL-level SEC | RTL Verilog/SystemVerilog sources or SystemVerilog flists | `sec` |
+| RTL to Gate SEC | SystemVerilog design 1 and Verilog design 2, plus Liberty libraries | `sec` |
 
 LEC is the default verification mode. SEC is selected with
 `verification: sec` in YAML or `-v sec` / `--verification sec` on the command

docs/flags-spec.md

@@ -16,6 +16,7 @@ The SEC-specific flag surface is documented separately in
 | `lec` | Gate-level combinational equivalence checking | Verilog or Naja IF netlists plus Liberty/Python primitive libraries as needed. |
 | `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. |
 
 LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 `verification: sec` in YAML.
@@ -24,8 +25,13 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 
 | Flag | Meaning |
 | --- | --- |
+| `--verification <lec\|sec>`, `-v <lec\|sec>` | Select LEC or SEC. Defaults to `lec`. |
+| `--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. |
 | `-verilog` | Use Verilog Format. |
-| `-systemverilog`, `-sv` | Use SystemVerilog format. |
 | `-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. |
@@ -35,14 +41,21 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `--design2 <file...>` | Explicit source list for design 2 in multi-file Verilog mode. |
 | `--liberty <file...>`, `--lib <file...>` | Liberty library files. |
 | `--verilog_preprocessing` | Enable preprocessing for Verilog inputs. |
-| `--compact` | Per-PO analysis is skipped in case the design is different. |
+| `--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. |
+| `--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`. |
+| `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`. |
+| `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`. |
 | `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`. |
 | `py_tech_files` | list[string] | Python primitive loaders loaded through `SNLPyLoader`. |
@@ -57,12 +70,15 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or
 | `po_cnf_export_path` | string | Output directory for per-PO CNF export. Defaults to `po_cnfs`, or `po_cnfs_<scope>` in scoped `naja_if` mode. |
 | `compact_mode` | bool | Same behavior as `--compact`. |
 | `report_skipped_pos` | bool | Same behavior as `--report-skipped-pos`. |
-| `solver` | string | SAT solver selection. Supported values: `kissat`, `glucose`. If omitted, the implementation defaults to `kissat`. |
+| `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. |
+| `solver` | string | SAT solver selection: `kissat`, `glucose`, or `cadical`. Defaults to `kissat`. |
 
 Example:
 
 ```yaml
 format: verilog
+verification: lec
 input_paths:
   - [design0_part1.v, design0_part2.v]
   - [design1_part1.v, design1_part2.v]
@@ -80,3 +96,22 @@ cnf_export_path: ./miter.cnf
 po_cnf_export: true
 po_cnf_export_path: ./po_cnfs
 ```
+
+SEC `sv2v` example:
+
+```yaml
+format: sv2v
+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]
+liberty_files:
+  - stdcells.lib
+solver: kissat
+compact_mode: true
+report_skipped_pos: true
+```

docs/sec-flags-spec.md

@@ -20,6 +20,7 @@ Supported SEC flows:
 | --- | --- |
 | Gate-level SEC | Sequential gate-level Verilog/SystemVerilog netlists with Liberty/Python primitive libraries as needed. |
 | RTL-level SEC | RTL Verilog/SystemVerilog sources, including SystemVerilog flists with explicit tops. |
+| SystemVerilog-to-Verilog SEC (`sv2v`) | SystemVerilog design 1 and Verilog design 2 for RTL-vs-gate comparison. |
 
 ## CLI Shape
 
@@ -66,8 +67,10 @@ kepler-formal -sv2v \
   --design1 rtl_pkg.sv rtl_top.sv \
   --design2 gate_top.v \
   -v sec \
+  -k 32 \
   --sec-engine pdr \
-  --sec-encoding dual_rail_steady
+  --sec-encoding dual_rail_steady \
+  --liberty stdcells.lib
 ```
 
 ## YAML Shape
@@ -97,7 +100,7 @@ liberty_files:
 
 | CLI flag | YAML key | Default | Values | Effect |
 | --- | --- | --- | --- | --- |
-| `-v sec`, `--verification sec` | `verification: sec` | `lec` | `lec`, `sec` | Selects SEC instead of combinational LEC. Values are lowercase. |
+| `-v <lec\|sec>`, `--verification <lec\|sec>` | `verification: <lec\|sec>` | `lec` | `lec`, `sec` | Selects combinational LEC or sequential SEC. Values are lowercase. |
 | `-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. |
@@ -246,7 +249,7 @@ SEC still depends on the normal front-end and library flags:
 | `--sv_design1_top`, `--sv_design2_top` | Per-design SystemVerilog top names. In `sv2v` mode, only `--sv_design1_top` is accepted. |
 | `--liberty`, `--lib`, `liberty_files` | Liberty primitives, including structured memory information used during SEC extraction. |
 | `py_tech_files` | Python primitive loaders. Must be provided through YAML, not through `--liberty`. |
-| `solver: kissat|glucose` | SAT solver used by the selected SEC engine. |
+| `solver: kissat|glucose|cadical` | SAT solver used by the selected SEC engine. This selector is YAML-only. |
 | `log_file` | Run log path. SEC defaults to `miter_log_<n>.txt` when no path is provided. |
 
 ## Known Construction Notes

docs/systemverilog/README.md

@@ -6,7 +6,7 @@ Status:
 
 - supported for RTL-level and gate-level SEC
 - supported through direct source lists or flists with explicit tops
-- LEC and non-SEC SystemVerilog coverage may still evolve with the frontend
+- SystemVerilog and `sv2v` input modes require SEC verification
 
 ## Current scope
 
@@ -29,16 +29,19 @@ Current entry points include:
 
 ```bash
 # Classic (single file per design)
-build/src/bin/kepler-formal <-systemverilog/-sv> [--verilog_preprocessing] <netlist1> <netlist2> [<library-file>...]
+build/src/bin/kepler-formal <-systemverilog/-sv> -v sec [--verilog_preprocessing] \
+  <netlist1> <netlist2> [<library-file>...]
 
 # Multi-file SystemVerilog designs
-build/src/bin/kepler-formal <-systemverilog/-sv> [--verilog_preprocessing] --design1 <file...> --design2 <file...> \
+build/src/bin/kepler-formal <-systemverilog/-sv> -v sec [--verilog_preprocessing] \
+  --design1 <file...> --design2 <file...> \
   [--liberty <library-file>...]
 
 # slang flists with explicit tops
-build/src/bin/kepler-formal -systemverilog \
+build/src/bin/kepler-formal -systemverilog -v sec \
   --sv_design1_flist <file> --sv_design1_top <name> \
-  --sv_design2_flist <file> --sv_design2_top <name>
+  --sv_design2_flist <file> --sv_design2_top <name> \
+  [--liberty <library-file>...]
 
 # RTL SystemVerilog vs gate-level Verilog for SEC
 build/src/bin/kepler-formal -sv2v -v sec \
@@ -51,7 +54,7 @@ build/src/bin/kepler-formal -sv2v -v sec \
   [--liberty <library-file>...]
 ```
 
-`--verilog_preprocessing` is also accepted as `--verilog-preprocessing`.
+The preprocessing flag is spelled `--verilog_preprocessing`.
 
 ## Flist mode
 
@@ -89,11 +92,15 @@ Multi-file SystemVerilog example:
 ```yaml
 format: systemverilog
 verification: sec
+max_k: 32
+sec_engine: pdr
+sec_encoding: dual_rail_steady
 input_paths:
   - [design0_pkg.sv, design0_top.sv]
   - [design1_pkg.sv, design1_top.sv]
 liberty_files:
   - stdcells.lib.gz
+py_tech_files:
   - primitives.py
 ```
 
@@ -102,6 +109,9 @@ Flist example:
 ```yaml
 format: systemverilog
 verification: sec
+max_k: 32
+sec_engine: pdr
+sec_encoding: dual_rail_steady
 sv_design1_flist: /path/to/design1.f
 sv_design1_top: top1
 sv_design2_flist: /path/to/design2.f
@@ -115,6 +125,7 @@ SV2V SEC example:
 ```yaml
 format: sv2v
 verification: sec
+max_k: 32
 sec_engine: pdr
 sec_encoding: dual_rail_steady
 input_paths:

example/README.md

@@ -14,6 +14,12 @@
 ../build/src/bin/kepler-formal -naja_if tinyrocket_naja.if tinyrocket_naja_edited.if \
   NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib fakeram45_64x15.lib
 
+## Verilog SEC example
+../build/src/bin/kepler-formal -verilog -v sec -k 32 \
+  --sec-engine pdr --sec-encoding dual_rail_steady \
+  tinyrocket.v tinyrocket_edited.v \
+  NangateOpenCellLibrary_typical.lib fakeram45_1024x32.lib fakeram45_64x32.lib fakeram45_64x15.lib
+
 # Through config file
 
 ## LEC YAML example