From 907d13c79e03dbea72d2fc1939c29cb9ff92468e Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Sun, 26 Jul 2026 11:19:10 +0200 Subject: [PATCH 1/2] docs: refresh SEC and sv2v configuration examples --- README.md | 1 + docs/flags-spec.md | 41 +++++++++++++++++++++++++++++++++--- docs/sec-flags-spec.md | 9 +++++--- docs/systemverilog/README.md | 23 ++++++++++++++------ example/README.md | 6 ++++++ 5 files changed, 68 insertions(+), 12 deletions(-) diff --git a/README.md b/README.md index b26dd730..9d49af50 100644 --- a/README.md +++ b/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` | +| SystemVerilog-to-Verilog SEC (`sv2v`) | 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 diff --git a/docs/flags-spec.md b/docs/flags-spec.md index 41b3a35e..3d75a6cc 100644 --- a/docs/flags-spec.md +++ b/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 `, `-v ` | Select LEC or SEC. Defaults to `lec`. | +| `--max-k `, `-k ` | Set the SEC proof/search bound. Defaults to `32`; SEC only. | +| `--sec-engine ` | Select the SEC engine. Defaults to `pdr`; SEC only. | +| `--sec-encoding ` | 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,7 +41,9 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or | `--design2 ` | Explicit source list for design 2 in multi-file Verilog mode. | | `--liberty `, `--lib ` | 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 `, `--sv_design2_flist ` | Per-design SystemVerilog file lists. Only design 1 is valid in `sv2v` mode. | +| `--sv_design1_top `, `--sv_design2_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 @@ -43,6 +51,11 @@ LEC is the default. Select SEC with `-v sec`, `--verification sec`, or | 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_` 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 +``` diff --git a/docs/sec-flags-spec.md b/docs/sec-flags-spec.md index 1760ba40..33359b7a 100644 --- a/docs/sec-flags-spec.md +++ b/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 `, `--verification ` | `verification: ` | `lec` | `lec`, `sec` | Selects combinational LEC or sequential SEC. Values are lowercase. | | `-k `, `--max-k ` | `max_k: ` | `32` | Non-negative integer | Sets the SEC proof/search bound. | | `--sec-engine ` | `sec_engine: ` | `pdr` | `k_induction`, `imc`, `pdr` | Selects the top-level SEC proof engine. Engine names are lowercase. | | `--sec-encoding ` | `sec_encoding: ` | `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_.txt` when no path is provided. | ## Known Construction Notes diff --git a/docs/systemverilog/README.md b/docs/systemverilog/README.md index c0b4739f..552aee2d 100644 --- a/docs/systemverilog/README.md +++ b/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] [...] +build/src/bin/kepler-formal <-systemverilog/-sv> -v sec [--verilog_preprocessing] \ + [...] # Multi-file SystemVerilog designs -build/src/bin/kepler-formal <-systemverilog/-sv> [--verilog_preprocessing] --design1 --design2 \ +build/src/bin/kepler-formal <-systemverilog/-sv> -v sec [--verilog_preprocessing] \ + --design1 --design2 \ [--liberty ...] # slang flists with explicit tops -build/src/bin/kepler-formal -systemverilog \ +build/src/bin/kepler-formal -systemverilog -v sec \ --sv_design1_flist --sv_design1_top \ - --sv_design2_flist --sv_design2_top + --sv_design2_flist --sv_design2_top \ + [--liberty ...] # 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 ...] ``` -`--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: diff --git a/example/README.md b/example/README.md index 4ba19031..7465fb42 100644 --- a/example/README.md +++ b/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 From cfb3b63e02c56e97dbf74905de666849bab70886 Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Sun, 26 Jul 2026 11:20:33 +0200 Subject: [PATCH 2/2] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 9d49af50..13645190 100644 --- a/README.md +++ b/README.md @@ -27,7 +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` | -| SystemVerilog-to-Verilog SEC (`sv2v`) | SystemVerilog design 1 and Verilog design 2, plus Liberty libraries | `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