flags-spec.md

Full Flag Specification

This document captures the current command-line and YAML configuration surface accepted by kepler-formal.

The stable top-level overview remains in README.md. The SEC-specific flag surface is documented separately in sec-flags-spec.md.

Verification modes

kepler-formal supports full equivalence checking flows:

Mode	Typical use	Inputs
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.

LEC is the default. Select SEC with -v sec, --verification sec, or verification: sec in YAML.

Binary flags

Flag	Meaning
-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.
--help, -h	Print usage and exit.
--config <file>, -c <file>	Load a YAML config file. If present anywhere on the CLI, YAML parsing takes precedence over the rest of the arguments.
--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.
--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.
--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.
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.
verilog_preprocessing	bool	Enable preprocessing for Verilog inputs.
log_level	string	debug and info are handled explicitly. Other values currently fall back to info.
log_file	string	Output path for the miter log file. If omitted, the tool writes miter_log_<n>.txt in the current working directory.
use_scopes	bool	Enable scoped verification for naja_if inputs.
clean_scopes	bool	Clean extracted scopes before scoped verification. Used with use_scopes.
cnf_export	bool	Enable CNF export.
cnf_export_path	string	Output path for CNF export. Defaults to miter.cnf, or miter_<scope>.cnf in scoped naja_if mode.
po_cnf_export	bool	Enable per-primary-output CNF export for each compared top.
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.

Example:

format: verilog
input_paths:
  - [design0_part1.v, design0_part2.v]
  - [design1_part1.v, design1_part2.v]
liberty_files:
  - library_file0.lib
  - library_file1.lib
py_tech_files:
  - primitives.py
verilog_preprocessing: true
solver: kissat
compact_mode: true
report_skipped_pos: true
cnf_export: true
cnf_export_path: ./miter.cnf
po_cnf_export: true
po_cnf_export_path: ./po_cnfs