mod aig2ir;
mod aig2v;
mod aig_equiv;
mod aig_eval;
mod aig_ir_equiv;
mod aig_stats;
mod block2fn;
mod common;
mod dslx2ir;
mod dslx2pipeline;
mod dslx2pipeline_eco;
mod dslx2sv_types;
mod dslx_equiv;
mod dslx_fn_eval;
mod dslx_fn_prove_assertions;
mod dslx_g8r_stats;
mod dslx_list_fns;
mod dslx_show;
#[cfg(feature = "unstable-dslx-specialize")]
mod dslx_specialize;
mod dslx_stitch_pipeline;
mod flag_defaults;
mod fn_eval;
mod fn_type_arg;
mod g8r2ir;
mod g8r2v;
mod g8r_cli;
mod g8r_equiv;
mod g8r_ir_equiv;
mod g8r_table;
mod gate_ir_equiv;
mod gv2aig;
mod gv2block;
mod gv2ir;
mod gv_dump_cone;
mod gv_instance_csv;
mod gv_read_stats;
mod ir2combo;
mod ir2delayinfo;
mod ir2gates;
mod ir2opt;
mod ir2pipeline;
mod ir_aig_sharing;
mod ir_annotate_ranges;
mod ir_bool_cones;
mod ir_diverse_samples;
mod ir_equiv;
mod ir_equiv_blocks;
mod ir_fn_autocov;
mod ir_fn_cone_extract;
mod ir_fn_eval;
mod ir_fn_mffcs;
mod ir_fn_node_count;
mod ir_fn_node_count_corpus;
mod ir_fn_structural_hash;
mod ir_fn_to_block;
mod ir_fn_to_dslx;
mod ir_fn_to_json;
mod ir_fn_to_z3_smtlib;
mod ir_ged;
mod ir_inline;
mod ir_localized_eco;
mod ir_mcmc_opt;
mod ir_op_histo;
mod ir_query;
mod ir_query_corpus;
mod ir_rewrite;
mod ir_round_trip;
mod ir_strip_pos_data;
mod ir_structural_similarity;
mod lib2proto;
mod lib_query;
mod proofs;
mod prove_enum_in_bound;
mod prove_quickcheck;
mod prover;
mod prover_config;
mod report_cli_error;
mod run_verilog_pipeline;
mod toolchain_config;
mod tools;
use crate::toolchain_config::ToolchainConfig;
use clap;
use clap::{Arg, ArgAction};
use once_cell::sync::Lazy;
use report_cli_error::report_cli_error_and_exit;
use serde::Deserialize;
use xlsynth::sv_bridge_builder::{SvEnumCaseNamingPolicy, SvStructFieldOrderingPolicy};
use xlsynth_prover::prover::types::AssertionSemantics;
use xlsynth_prover::prover::types::QuickCheckAssertionSemantics;
static DEFAULT_ADDER_MAPPING: Lazy<String> =
Lazy::new(|| xlsynth_g8r::ir2gate_utils::AdderMapping::default().to_string());
#[derive(Deserialize)]
struct XlsynthToolchain {
toolchain: ToolchainConfig,
}
trait AppExt {
fn add_delay_model_arg(self) -> Self;
fn add_pipeline_args(self) -> Self;
fn add_dslx_input_args(self, include_top: bool) -> Self;
fn add_codegen_args(self) -> Self;
fn add_bool_arg(self, long: &'static str, help: &'static str) -> Self;
fn add_ir_top_arg(self, required: bool) -> Self;
fn add_g8r_lowering_flags(self) -> Self;
}
impl AppExt for clap::Command {
fn add_delay_model_arg(self) -> Self {
(self as clap::Command).arg(
Arg::new("DELAY_MODEL")
.long("delay_model")
.value_name("DELAY_MODEL")
.help("The delay model to use")
.required(true)
.action(ArgAction::Set),
)
}
fn add_dslx_input_args(self, include_top: bool) -> Self {
let mut command = (self as clap::Command).arg(
Arg::new("dslx_input_file")
.long("dslx_input_file")
.value_name("DSLX_INPUT_FILE")
.help("The input DSLX file")
.required(true)
.action(ArgAction::Set),
);
if include_top {
command = command.arg(
Arg::new("dslx_top")
.long("dslx_top")
.value_name("DSLX_TOP")
.help("The top-level entry point")
.required(true),
)
}
command = command
.arg(
Arg::new("dslx_path")
.long("dslx_path")
.value_name("DSLX_PATH_SEMI_SEPARATED")
.help("Semi-separated paths for DSLX")
.action(ArgAction::Set),
)
.arg(
Arg::new("dslx_stdlib_path")
.long("dslx_stdlib_path")
.value_name("DSLX_STDLIB_PATH")
.help("Path to the DSLX standard library")
.action(ArgAction::Set),
);
command.add_bool_arg("warnings_as_errors", "Treat warnings as errors")
}
fn add_pipeline_args(self) -> Self {
(self as clap::Command)
.arg(
Arg::new("pipeline_stages")
.long("pipeline_stages")
.value_name("PIPELINE_STAGES")
.help("Number of pipeline stages")
.action(ArgAction::Set),
)
.arg(
Arg::new("clock_period_ps")
.long("clock_period_ps")
.value_name("CLOCK_PERIOD_PS")
.help("Clock period in picoseconds")
.action(ArgAction::Set),
)
}
fn add_bool_arg(self, long: &'static str, help: &'static str) -> Self {
(self as clap::Command).arg(
Arg::new(long)
.long(long)
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help(help),
)
}
fn add_codegen_args(self) -> Self {
let result = (self as clap::Command)
.arg(
Arg::new("module_name")
.long("module_name")
.value_name("MODULE_NAME")
.help("Name of the generated module"),
)
.arg(
Arg::new("input_valid_signal")
.long("input_valid_signal")
.value_name("INPUT_VALID_SIGNAL")
.help("Load enable signal for pipeline registers"),
)
.arg(
Arg::new("output_valid_signal")
.long("output_valid_signal")
.value_name("OUTPUT_VALID_SIGNAL")
.help("Output port holding pipelined valid signal"),
);
result
.add_bool_arg(
"flop_inputs",
"Whether to flop input ports (vs leaving combinational delay into the I/Os)",
)
.add_bool_arg(
"flop_outputs",
"Whether to flop output ports (vs leaving combinational delay into the I/Os)",
)
.add_bool_arg("add_idle_output", "Add an idle output port")
.add_bool_arg(
"add_invariant_assertions",
"Add assertions for invariants in generated code",
)
.add_bool_arg("array_index_bounds_checking", "Array index bounds checking")
.add_bool_arg("separate_lines", "Separate lines in generated code")
.add_bool_arg(
"use_system_verilog",
"Whether to emit System Verilog instead of Verilog",
)
.arg(
Arg::new("reset")
.long("reset")
.value_name("RESET")
.help("Reset signal name"),
)
.add_bool_arg("reset_asynchronous", "Reset is asynchronous")
.add_bool_arg("reset_active_low", "Reset is active low")
.add_bool_arg(
"reset_data_path",
"Reset datapath registers as well as valid signals",
)
.arg(
Arg::new("output_schedule_path")
.long("output_schedule_path")
.value_name("OUTPUT_SCHEDULE_PATH")
.help("Write schedule proto text to this path"),
)
.arg(
Arg::new("output_verilog_line_map_path")
.long("output_verilog_line_map_path")
.value_name("OUTPUT_VERILOG_LINE_MAP_PATH")
.help("Write Verilog line map textproto to this path"),
)
.arg(
Arg::new("output_block_ir_path")
.long("output_block_ir_path")
.value_name("OUTPUT_BLOCK_IR_PATH")
.help("Write block IR text to this path"),
)
.arg(
Arg::new("output_residual_data_path")
.long("output_residual_data_path")
.value_name("OUTPUT_RESIDUAL_DATA_PATH")
.help("Write residual data to this path"),
)
.arg(
Arg::new("reference_residual_data_path")
.long("reference_residual_data_path")
.value_name("REFERENCE_RESIDUAL_DATA_PATH")
.help("Path to reference residual data for comparison"),
)
}
fn add_ir_top_arg(self, required: bool) -> Self {
(self as clap::Command).arg(
Arg::new("ir_top")
.long("top")
.value_name("TOP")
.help("The top-level entry point to use for the IR")
.required(required)
.action(ArgAction::Set),
)
}
fn add_g8r_lowering_flags(self) -> Self {
(self as clap::Command)
.add_bool_arg("fold", "Fold the gate representation")
.add_bool_arg("hash", "Hash the gate representation")
.add_bool_arg(
"enable-rewrite-carry-out",
"Enable carry-out rewrite in prep_for_gatify (introduces ext_carry_out)",
)
.add_bool_arg(
"enable-rewrite-prio-encode",
"Enable prio-encode / CLZ rewrites in prep_for_gatify (introduces ext_prio_encode / ext_clz)",
)
.add_bool_arg(
"enable-rewrite-nary-add",
"Enable nary-add rewrites in prep_for_gatify (recovers gated inc/dec helpers and grows ext_nary_add to a fixed point)",
)
.add_bool_arg(
"enable-rewrite-mask-low",
"Enable mask-low rewrite in prep_for_gatify (introduces ext_mask_low)",
)
.arg(
clap::Arg::new("adder_mapping")
.long("adder-mapping")
.value_name("ADDER_MAPPING")
.help("The adder mapping strategy to use (default: brent-kung).")
.value_parser(["ripple-carry", "brent-kung", "kogge-stone"])
.default_value(DEFAULT_ADDER_MAPPING.as_str())
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("mul_adder_mapping")
.long("mul-adder-mapping")
.value_name("ADDER_MAPPING")
.help(
"Optional override for the adder mapping strategy used inside multipliers. If not set, inherits --adder-mapping.",
)
.value_parser(["ripple-carry", "brent-kung", "kogge-stone"])
.action(clap::ArgAction::Set),
)
.add_bool_arg("fraig", "Run fraig optimization")
.arg(
clap::Arg::new("fraig_max_iterations")
.long("fraig-max-iterations")
.value_name("N")
.help("Maximum number of iterations for fraig optimization")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_fraig_sim_samples")
.long("max-fraig-sim-samples")
.alias("fraig-sim-samples")
.default_value("8192")
.value_name("N")
.help("Maximum number of random simulation samples to use for FRAIG candidate discovery")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("gate_formal_backend")
.long("gate-formal-backend")
.value_name("BACKEND")
.help("Formal backend for gate-level proof steps (default: cadical)")
.value_parser(["cadical", "varisat", "z3", "ir"])
.default_value("cadical")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"compute_graph_logical_effort",
"Compute the graph logical effort worst case delay",
)
.arg(
clap::Arg::new("graph_logical_effort_beta1")
.long("graph-logical-effort-beta1")
.value_name("BETA1")
.help("Beta1 value for graph logical effort computation (default 1.0)")
.default_value("1.0")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("graph_logical_effort_beta2")
.long("graph-logical-effort-beta2")
.value_name("BETA2")
.help("Beta2 value for graph logical effort computation (default 0.0)")
.default_value("0.0")
.action(clap::ArgAction::Set),
)
.arg(
Arg::new("toggle_sample_count")
.long("toggle-sample-count")
.value_name("N")
.help("If > 0, generate N random input samples and print toggle stats.")
.default_value("0")
.action(ArgAction::Set),
)
.arg(
Arg::new("toggle_sample_seed")
.long("toggle-seed")
.value_name("SEED")
.help("Seed for random toggle stimulus (default 0)")
.default_value("0")
.action(ArgAction::Set),
)
}
}
fn main() {
let _ = env_logger::try_init();
log::info!(
"xlsynth-driver starting; version: {}",
env!("CARGO_PKG_VERSION")
);
let cmd = clap::Command::new("xlsynth-driver")
.version(env!("CARGO_PKG_VERSION"))
.about("Command line driver for XLS/xlsynth capabilities")
.arg(
Arg::new("toolchain")
.long("toolchain")
.value_name("TOOLCHAIN")
.help("Path to a xlsynth-toolchain.toml file")
.action(ArgAction::Set),
)
.subcommand(clap::Command::new("version").about("Prints the version of the driver"))
.subcommand(
clap::Command::new("ir-diverse-samples")
.about("Selects a diverse subset of IR samples from a corpus directory")
.arg(
clap::Arg::new("corpus_dir")
.value_name("CORPUS_DIR")
.help("Root directory to search recursively for .ir files")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("signature_depth")
.long("signature-depth")
.value_name("N")
.help("Depth for structural signature hashing (default 2)")
.required(false)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("make_symlink_dir")
.long("make-symlink-dir")
.value_name("DIR")
.help(
"If set, create DIR (must be empty if it exists) and populate it with symlinks to each selected sample",
)
.required(false)
.action(ArgAction::Set),
)
.add_bool_arg(
"log-skipped",
"Log skipped samples (read/parse/lower failures) to stderr via the logger",
)
.add_bool_arg(
"explain-new-hashes",
"Print the PIR node signatures that introduced new hashes for each selected sample",
),
)
.subcommand(
clap::Command::new("dslx2pipeline")
.about("Converts DSLX to SystemVerilog")
.arg(
clap::Arg::new("output_unopt_ir")
.long("output_unopt_ir")
.value_name("PATH")
.help("Path to write the unoptimized IR (package) output")
.required(false)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("output_opt_ir")
.long("output_opt_ir")
.value_name("PATH")
.help("Path to write the optimized IR (package) output")
.required(false)
.action(ArgAction::Set),
)
.add_delay_model_arg()
.add_dslx_input_args(true)
.add_pipeline_args()
.add_codegen_args()
.add_bool_arg("keep_temps", "Keep temporary files")
.add_bool_arg(
"type_inference_v2",
"Enable the experimental type-inference v2 algorithm",
),
)
.subcommand(
clap::Command::new("dslx-stitch-pipeline")
.about("Stitches DSLX pipeline stages")
.add_dslx_input_args(false)
.arg(
Arg::new("dslx_top")
.long("dslx_top")
.value_name("DSLX_TOP")
.help("Top-level pipeline prefix for implicit <top>_cycleN discovery; ignored when --stages is used")
.conflicts_with("stages")
.required_unless_present("stages"),
)
.add_bool_arg(
"use_system_verilog",
"Whether to emit SystemVerilog (default true; set to false for plain Verilog)",
)
.arg(
Arg::new("input_valid_signal")
.long("input_valid_signal")
.value_name("INPUT_VALID_SIGNAL")
.help("Load enable signal for pipeline registers"),
)
.arg(
Arg::new("output_valid_signal")
.long("output_valid_signal")
.value_name("OUTPUT_VALID_SIGNAL")
.help("Output port holding pipelined valid signal"),
)
.arg(
Arg::new("reset")
.long("reset")
.value_name("RESET")
.help("Reset signal name"),
)
.add_bool_arg(
"reset_active_low",
"Reset is active low",
)
.arg(
Arg::new("stages")
.long("stages")
.value_name("CSV")
.help("Comma-separated explicit stage names in order (overrides automatic _cycle indexing)")
.action(ArgAction::Set),
)
.arg(
Arg::new("output_module_name")
.long("output_module_name")
.value_name("NAME")
.help("Wrapper module name; required with --stages. Defaults to --dslx_top when using implicit discovery."),
)
.add_bool_arg(
"flop_inputs",
"Whether to insert input pipeline flops (default true)",
)
.add_bool_arg(
"flop_outputs",
"Whether to insert output pipeline flops (default true)",
)
.add_bool_arg(
"array_index_bounds_checking",
"Whether to emit array index bounds checking",
),
)
.subcommand(
clap::Command::new("dslx-fn-eval")
.about("Evaluates a DSLX function for each tuple in an .irvals file; prints one output per line")
.add_dslx_input_args(true)
.arg(
clap::Arg::new("input_ir_path")
.long("input_ir_path")
.value_name("PATH")
.help("Path to an .irvals file with one typed IR tuple value per line")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("eval_mode")
.long("eval_mode")
.value_name("MODE")
.help("Evaluation backend: interp|jit|pir-interp (default interp)")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("pir_dump_node_values")
.long("pir_dump_node_values")
.help(
"When using --eval_mode=pir-interp, dump all intermediate PIR node values to stdout",
)
.action(ArgAction::SetTrue),
),
)
.subcommand(
clap::Command::new("dslx-fn-prove-assertions")
.about("Prove that assertions reachable from a DSLX function cannot fail")
.add_dslx_input_args(true)
.arg(
clap::Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Select solver backend")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("assert_label_filter")
.long("assert-label-filter")
.value_name("REGEX")
.help("Include only assertions whose label matches this regex (use `|` to combine labels)")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"assume-enum-in-bound",
"Constrain enum-typed top parameters to declared enum values (default true)",
)
.arg(
clap::Arg::new("uf")
.long("uf")
.value_name("func_name:uf_name")
.help("Treat DSLX function as uninterpreted: format <func_name>:<uf_name> (repeatable). Assertions inside mapped functions are ignored.")
.action(clap::ArgAction::Append),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("dslx2ir")
.about("Converts DSLX to IR")
.add_dslx_input_args(false)
.arg(
Arg::new("dslx_top")
.long("dslx_top")
.value_name("DSLX_TOP")
.help("The top-level entry point")
.required_if_eq("opt", "true"),
)
.arg(
Arg::new("opt")
.long("opt")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("Optimize the IR we emit as well")
)
.arg(
Arg::new("aug_opt")
.long("aug-opt")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("Use augmented optimizer sandwich when --opt=true (default: false)"),
)
.add_bool_arg(
"type_inference_v2",
"Enable the experimental type-inference v2 algorithm",
)
.add_bool_arg(
"convert_tests",
"Convert test procs/functions to IR",
)
)
.subcommand(
clap::Command::new("dslx-show")
.about("Resolve and print a DSLX symbol definition (enums/structs/type aliases/constants/functions/quickchecks)")
.arg(
clap::Arg::new("dslx_input_file")
.long("dslx_input_file")
.value_name("DSLX_INPUT_FILE")
.help("Optional input DSLX file - if omitted, symbol must be qualified like 'path.with.dots::Name'")
.required(false)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("dslx_path")
.long("dslx_path")
.value_name("DSLX_PATH_SEMI_SEPARATED")
.help("Semi-separated paths for DSLX lookup (used for imported/library symbols)")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("dslx_stdlib_path")
.long("dslx_stdlib_path")
.value_name("DSLX_STDLIB_PATH")
.help("Path to the DSLX standard library")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("symbol")
.value_name("SYMBOL")
.help("Symbol to show; supports dotted module path + member like 'foo.bar.baz::Name', or just 'Name' with --dslx_input_file")
.required(true)
.index(1)
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("dslx-list-fns")
.about("Lists DSLX functions with parametric/concrete metadata in structured form")
.arg(
clap::Arg::new("dslx_input_file")
.long("dslx_input_file")
.value_name("DSLX_INPUT_FILE")
.help("Input DSLX file to inspect")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("dslx_path")
.long("dslx_path")
.value_name("DSLX_PATH_SEMI_SEPARATED")
.help("Semi-separated paths for DSLX lookup")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("dslx_stdlib_path")
.long("dslx_stdlib_path")
.value_name("DSLX_STDLIB_PATH")
.help("Path to the DSLX standard library")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("format")
.long("format")
.value_name("FORMAT")
.help("Output format: jsonl (default) or json")
.value_parser(["jsonl", "json"])
.default_value("jsonl")
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("dslx2sv-types")
.about("Converts DSLX type definitions to SystemVerilog")
.add_dslx_input_args(false)
.arg(
Arg::new("sv_enum_case_naming_policy")
.long("sv_enum_case_naming_policy")
.value_name("POLICY")
.help(
"Enum case naming policy for generated SystemVerilog enum members",
)
.required(true)
.action(ArgAction::Set)
.value_parser(clap::builder::EnumValueParser::<
SvEnumCaseNamingPolicy,
>::new()),
)
.arg(
Arg::new("sv_struct_field_ordering")
.long("sv_struct_field_ordering")
.value_name("POLICY")
.help(
"Packed-struct layout policy for generated SystemVerilog packed structs; member order controls the packed bit layout",
)
.default_value("as_declared")
.action(ArgAction::Set)
.value_parser(clap::builder::EnumValueParser::<
SvStructFieldOrderingPolicy,
>::new()),
),
)
.subcommand(
clap::Command::new("dslx-g8r-stats")
.about("Emit gate-level summary stats for a DSLX entry point")
.add_dslx_input_args(true)
.add_g8r_lowering_flags()
.add_bool_arg(
"type_inference_v2",
"Enable the experimental type-inference v2 algorithm",
),
)
.subcommand(
clap::Command::new("ir-inline")
.about("Converts IR to call-inlined IR")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("ir_top")
.long("top")
.value_name("TOP")
.help("The top-level entry point; defaults to the package top function when present, or the only function when unique, and is otherwise required")
.action(ArgAction::Set),
)
.arg(
Arg::new("unroll")
.long("unroll")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.default_value("true")
.help("Also unroll counted_for nodes while inlining (default: true)"),
),
)
.subcommand(
clap::Command::new("ir2opt")
.about("Converts IR to optimized IR")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("ir_top")
.long("top")
.value_name("TOP")
.help("The top-level entry point")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("aug_opt")
.long("aug-opt")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("Enable the augmented optimizer sandwich (default: false)"),
),
)
.subcommand(
xlsynth_mcmc_pir::driver_cli::add_pir_mcmc_args(
clap::Command::new("ir-mcmc-opt")
.about("Optimizes PIR IR with MCMC and emits best artifacts"),
),
)
.subcommand(
clap::Command::new("ir2pipeline")
.about("Converts IR to a pipeline")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_delay_model_arg()
.add_ir_top_arg(false)
.add_codegen_args()
.add_pipeline_args()
.add_bool_arg("opt", "Optimize the IR before scheduling pipeline")
.arg(
Arg::new("aug_opt")
.long("aug-opt")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("Use augmented optimizer sandwich when --opt=true (default: false)"),
)
.add_bool_arg("keep_temps", "Keep temporary files"),
)
.subcommand(
clap::Command::new("ir2combo")
.about("Converts IR to combinational SystemVerilog")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_delay_model_arg()
.add_ir_top_arg(false)
.add_codegen_args()
.add_bool_arg("opt", "Optimize the IR before codegen")
.arg(
Arg::new("aug_opt")
.long("aug-opt")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("Use augmented optimizer sandwich when --opt=true (default: false)"),
)
.add_bool_arg("keep_temps", "Keep temporary files"),
)
.subcommand(
clap::Command::new("ir-fn-to-block")
.about("Converts an IR function to Block IR (requires external toolchain)")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(true),
)
.subcommand(
clap::Command::new("ir-fn-to-dslx")
.about("Converts an IR function to DSLX function text")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(true)
.arg(
Arg::new("verify_roundtrip")
.long("verify-roundtrip")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help(
"Convert emitted DSLX back to IR and prove equivalence against input IR",
),
),
)
.subcommand(
clap::Command::new("ir2delayinfo")
.about("Converts IR entry point to delay info output")
.add_delay_model_arg()
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("ir_top")
.help("The top-level entry point")
.required(true)
.index(2),
),
)
.subcommand(
clap::Command::new("ir-equiv")
.about("Checks if two IRs are equivalent")
.arg(
Arg::new("lhs_ir_file")
.help("The left-hand side IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("rhs_ir_file")
.help("The right-hand side IR file")
.required(true)
.index(2),
)
.add_ir_top_arg(false)
.arg(
Arg::new("lhs_ir_top")
.long("lhs_ir_top")
.help("The top-level entry point for the left-hand side IR"),
)
.arg(
Arg::new("rhs_ir_top")
.long("rhs_ir_top")
.help("The top-level entry point for the right-hand side IR"),
)
.arg(
Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking (requires --features=with-easy-smt)")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(ArgAction::Set),
)
.add_bool_arg(
"flatten_aggregates",
"Flatten tuple and array types to bits for equivalence checking",
)
.arg(
Arg::new("drop_params")
.long("drop_params")
.help("Comma-separated list of parameter names to drop from both functions before equivalence checking")
.action(ArgAction::Set),
)
.arg(
Arg::new("parallelism_strategy")
.long("parallelism-strategy")
.value_name("STRATEGY")
.help("Parallelism strategy")
.value_parser(["single-threaded", "output-bits", "input-bit-split"])
.default_value("single-threaded")
.action(ArgAction::Set),
)
.arg(
Arg::new("assertion_semantics")
.long("assertion-semantics")
.value_name("SEMANTICS")
.help("Assertion semantics")
.value_parser(clap::value_parser!(AssertionSemantics))
.default_value("ignore")
.action(ArgAction::Set),
)
.arg(
Arg::new("assert_label_filter")
.long("assert-label-filter")
.value_name("REGEX")
.help("Include only assertions whose label matches this regex (use `|` to combine labels)")
.action(ArgAction::Set),
)
.add_bool_arg(
"lhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the LHS IR, useful when only LHS or RHS has implicit token",
)
.add_bool_arg(
"rhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the RHS IR, useful when only LHS or RHS has implicit token",
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-equiv-blocks")
.about("Checks if two IR blocks are equivalent")
.arg(
Arg::new("lhs_ir_file")
.help("The left-hand side IR block file")
.required(true)
.index(1),
)
.arg(
Arg::new("rhs_ir_file")
.help("The right-hand side IR block file")
.required(true)
.index(2),
)
.arg(
Arg::new("lhs_top")
.long("lhs_top")
.help("Top-level block name for the left-hand side IR"),
)
.arg(
Arg::new("rhs_top")
.long("rhs_top")
.help("Top-level block name for the right-hand side IR"),
)
.arg(
Arg::new("top")
.long("top")
.help("Top-level block name for both IRs"),
)
.arg(
Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking (requires --features=with-easy-smt)")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(ArgAction::Set),
)
.add_bool_arg(
"flatten_aggregates",
"Flatten tuple and array types to bits for equivalence checking",
)
.arg(
Arg::new("drop_params")
.long("drop_params")
.help("Comma-separated list of parameter names to drop from both functions before equivalence checking")
.action(ArgAction::Set),
)
.arg(
Arg::new("parallelism_strategy")
.long("parallelism-strategy")
.value_name("STRATEGY")
.help("Parallelism strategy")
.value_parser(["single-threaded", "output-bits", "input-bit-split"])
.default_value("single-threaded")
.action(ArgAction::Set),
)
.arg(
Arg::new("assertion_semantics")
.long("assertion-semantics")
.value_name("SEMANTICS")
.help("Assertion semantics")
.value_parser(clap::value_parser!(AssertionSemantics))
.default_value("ignore")
.action(ArgAction::Set),
)
.add_bool_arg(
"lhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the LHS IR, useful when only LHS or RHS has implicit token",
)
.add_bool_arg(
"rhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the RHS IR, useful when only LHS or RHS has implicit token",
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-ged")
.about("Tells the Graph Edit Distance between two IR functions")
.arg(
Arg::new("lhs_ir_file")
.help("The left-hand side IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("rhs_ir_file")
.help("The right-hand side IR file")
.required(true)
.index(2),
)
.arg(
Arg::new("lhs_ir_top")
.long("lhs_ir_top")
.help("The top-level entry point for the left-hand side IR"),
)
.arg(
Arg::new("rhs_ir_top")
.long("rhs_ir_top")
.help("The top-level entry point for the right-hand side IR"),
)
.add_bool_arg("json", "Output in JSON format"),
)
.subcommand(
clap::Command::new("ir-query")
.about("Matches an IR query expression against a top function")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("query")
.help("The IR query expression")
.required(true)
.index(2),
)
.add_bool_arg(
"check_query",
"Validate the query and exit without reading/parsing IR (useful for preflight before corpus scans)",
)
.add_bool_arg(
"show-file",
"Prefix each match with the input file path as '<path>: <match>'",
)
.add_bool_arg(
"show-ret",
"Prefix matches that are return values with 'ret' (true by default)",
)
.arg(
Arg::new("ir_top")
.long("top")
.help("Top-level function name (overrides package top)"),
),
)
.subcommand(
clap::Command::new("ir-rewrite")
.about("Rewrites all IR nodes matching a query expression in a function")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("match")
.help("The IR query expression to match")
.required(true)
.index(2),
)
.arg(
Arg::new("replacement")
.help("The rewrite template to substitute for matches")
.required(true)
.index(3),
)
.arg(
Arg::new("target")
.long("target")
.help("Exact rewrite target as NODE_ID or NODE_ID:OPERAND (zero-based operand slot)")
.value_name("NODE_ID[:OPERAND]"),
)
.arg(
Arg::new("ir_top")
.long("top")
.help("Function name to rewrite (overrides package top)"),
)
.arg(
Arg::new("must-match")
.long("must-match")
.help("Exit with an error if no matches are found")
.action(ArgAction::SetTrue),
),
)
.subcommand(
clap::Command::new("ir-query-corpus")
.about("Runs `ir-query` over every .ir file in a corpus directory (with fast prefiltering)")
.arg(
Arg::new("corpus_dir")
.help("Root corpus directory to scan recursively for .ir files")
.required(true)
.index(1),
)
.arg(
Arg::new("query")
.help("The IR query expression")
.required(true)
.index(2),
)
.arg(
Arg::new("ir_top")
.long("top")
.help("Top-level function name (overrides package top)"),
)
.add_bool_arg(
"show-ret",
"Prefix matches that are return values with 'ret' (true by default)",
)
.add_bool_arg(
"prefilter",
"Use a fast textual prefilter (based on operator names in the query) before parsing IR (true by default)",
)
.add_bool_arg(
"ignore-parse-errors",
"Skip files that fail PIR parse/validate instead of erroring out (true by default)",
)
.arg(
Arg::new("max-files")
.long("max-files")
.value_name("N")
.help("Stop after scanning N files (default: unlimited)")
.action(ArgAction::Set),
)
.arg(
Arg::new("max-matches")
.long("max-matches")
.value_name("N")
.help("Stop after emitting N matches (default: unlimited)")
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-op-histo")
.about("Computes an operation histogram for one IR file")
.arg(
Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("ir_top")
.long("top")
.help("Top-level function name (overrides package top)"),
)
.add_bool_arg(
"include-types",
"Include operand/result types in histogram keys (true by default)",
),
)
.subcommand(
clap::Command::new("ir-op-histo-corpus")
.about("Computes per-file and total operation histograms for .ir files in a corpus")
.arg(
Arg::new("corpus_dir")
.help("Root corpus directory to scan recursively for .ir files")
.required(true)
.index(1),
)
.arg(
Arg::new("ir_top")
.long("top")
.help("Top-level function name (overrides package top)"),
)
.add_bool_arg(
"ignore-parse-errors",
"Skip files that fail PIR parse/validate instead of erroring out (true by default)",
)
.add_bool_arg(
"include-types",
"Include operand/result types in histogram keys (true by default)",
)
.arg(
Arg::new("max-files")
.long("max-files")
.value_name("N")
.help("Stop after scanning N files (default: unlimited)")
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-structural-similarity")
.about("Computes a depth-to-discrepancy histogram between two IR functions")
.arg(
Arg::new("lhs_ir_file")
.help("The left-hand side IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("rhs_ir_file")
.help("The right-hand side IR file")
.required(true)
.index(2),
)
.arg(
Arg::new("lhs_ir_top")
.long("lhs_ir_top")
.help("The top-level entry point for the left-hand side IR"),
)
.arg(
Arg::new("rhs_ir_top")
.long("rhs_ir_top")
.help("The top-level entry point for the right-hand side IR"),
)
.arg(
Arg::new("output_dir")
.long("output-dir")
.value_name("DIR")
.help("Directory to write outputs (original IR copies). If omitted, a temp directory is created and printed."),
)
.add_bool_arg(
"show_discrepancies",
"Show per-depth discrepancy signatures in verbose form",
),
)
.subcommand(
clap::Command::new("ir-localized-eco")
.about("Computes a localized ECO diff (old → new) and emits JSON edits and a summary")
.arg(
Arg::new("old_ir_file")
.help("The old/original IR file")
.required(true)
.index(1),
)
.arg(
Arg::new("new_ir_file")
.help("The new/target IR file")
.required(true)
.index(2),
)
.arg(
Arg::new("old_ir_top")
.long("old_ir_top")
.help("Top-level entry point for the old IR"),
)
.arg(
Arg::new("new_ir_top")
.long("new_ir_top")
.help("Top-level entry point for the new IR"),
)
.arg(
Arg::new("json_out")
.long("json_out")
.value_name("PATH")
.help("Write the JSON report to PATH; if omitted a temp file is created and its path is printed"),
)
.arg(
Arg::new("output_dir")
.long("output_dir")
.value_name("DIR")
.help("Directory to write outputs (JSON, patched .ir). If omitted, a temp directory is created and printed."),
)
.arg(
Arg::new("compute_text_diff")
.long("compute-text-diff")
.value_name("BOOL")
.help("Compute IR/RTL text diffs (expensive)")
.value_parser(["true", "false"]).num_args(1)
.default_value("false")
.action(ArgAction::Set),
)
.arg(
Arg::new("sanity_samples")
.long("sanity-samples")
.value_name("N")
.help("If > 0, run N randomized interpreter samples (in addition to all-zeros and all-ones) to sanity-check patched(old) vs new.")
.default_value("0"),
)
.arg(
Arg::new("sanity_seed")
.long("sanity-seed")
.value_name("SEED")
.help("Seed for randomized interpreter samples (default 0)")
.default_value("0"),
),
)
.subcommand(
clap::Command::new("ir-round-trip")
.about("Parses an IR file and writes it back out to stdout")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("strip_pos_attrs")
.long("strip-pos-attrs")
.value_name("BOOL")
.action(ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("If true, strip file_number and (future) node pos attributes from output"),
),
)
.subcommand(
clap::Command::new("ir-annotate-ranges")
.about("Reads an IR package and emits it with per-node range/known-bits annotations")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false),
)
.subcommand(
clap::Command::new("ir2gates")
.about("Converts IR to GateFn and emits it to stdout as JSON")
.arg(
clap::Arg::new("ir_input_file")
.value_name("IR_INPUT_FILE")
.help("The input IR file")
.required(true)
.action(ArgAction::Set),
)
.add_ir_top_arg(false)
.add_bool_arg("quiet", "Quiet mode")
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON summary to PATH")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("prepared_ir_out")
.long("prepared-ir-out")
.value_name("PATH")
.help("Write the residual PIR after prep_for_gatify to PATH")
.action(clap::ArgAction::Set),
)
.add_g8r_lowering_flags()
.add_bool_arg(
"emit-independent-op-stats",
"Emit independent-op (per-node) GateFn stats; can be expensive",
),
)
.subcommand(
clap::Command::new("ir2g8r")
.about("Converts IR to GateFn and emits it to stdout; optionally writes .g8rbin, netlist, and stats")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false)
.add_g8r_lowering_flags()
.arg(
clap::Arg::new("bin_out")
.long("bin-out")
.value_name("PATH")
.help("Path to write the .g8rbin file")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("aiger_out")
.long("aiger-out")
.value_name("PATH")
.help("Path to write the GateFn as AIGER; use .aag for ASCII or .aig for binary")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("stats_out")
.long("stats-out")
.value_name("PATH")
.help("Path to write the JSON summary statistics")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("netlist_out")
.long("netlist-out")
.value_name("PATH")
.help("Path to write the gate-level netlist (human-readable)")
.action(clap::ArgAction::Set),
)
)
.subcommand(
clap::Command::new("dslx2pipeline-eco")
.about("Produces Verilog with minimal edits from baseline_unopt_ir to current DSLX, using greedy GED edits; accepts dslx2pipeline args + --baseline_unopt_ir")
.arg(
clap::Arg::new("output_unopt_ir")
.long("output_unopt_ir")
.value_name("PATH")
.help("Path to write the unoptimized IR (package) output")
.required(false)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("output_opt_ir")
.long("output_opt_ir")
.value_name("PATH")
.help("Path to write the optimized IR (package) output")
.required(false)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("baseline_unopt_ir")
.long("baseline_unopt_ir")
.value_name("PATH")
.help("Path to the baseline unoptimized IR (package) before the source change")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("output_baseline_verilog_path")
.long("output_baseline_verilog_path")
.value_name("PATH")
.help("If set, write the baseline (pre-ECO) Verilog/SystemVerilog to PATH")
.required(false)
.action(ArgAction::Set),
)
.add_delay_model_arg()
.add_dslx_input_args(true)
.add_pipeline_args()
.add_codegen_args()
.add_bool_arg("keep_temps", "Keep temporary files")
.add_bool_arg(
"type_inference_v2",
"Enable the experimental type-inference v2 algorithm",
)
.arg(
clap::Arg::new("edits_debug_out")
.long("edits_debug_out")
.value_name("PATH")
.help("Write the debug string of IrEdits to PATH (optional)")
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("lib2proto")
.about("Converts Liberty file(s) to proto or textproto")
.arg(
Arg::new("liberty_files")
.help("Liberty file(s)")
.required(true)
.num_args(1..)
)
.arg(
Arg::new("output")
.long("output")
.help("Output file (.proto or .textproto)")
.required(true)
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("lib-query")
.about("Runs a rough XPath-like query over Liberty AST blocks and debug-prints matches")
.arg(
Arg::new("liberty_file")
.help("Input Liberty file (.lib or .lib.gz)")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("query")
.help("Query string, e.g. //cell[qual0='NAND2']//timing or //cell[matches(qual0, '^(NAND2|NOR2)$')]//timing")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("max_matches")
.long("max-matches")
.help("Maximum number of matches to print")
.default_value("20")
.value_parser(clap::value_parser!(usize))
.action(ArgAction::Set),
)
.arg(
Arg::new("path_only")
.long("path-only")
.help("Only print matched paths, not full Debug block dumps")
.action(ArgAction::SetTrue),
)
.arg(
Arg::new("jsonl")
.long("jsonl")
.help("Emit each match as one JSON line with fields: path, block")
.action(ArgAction::SetTrue),
),
)
.subcommand(
clap::Command::new("block2fn")
.about("Inlines a block and converts it to a PIR function")
.arg(
Arg::new("block_ir")
.long("block_ir")
.help("Input Block IR file")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("tie_input_ports")
.long("tie-input-ports")
.help("Comma-separated input ties (e.g., A=0,B=0b1011)")
.required(false)
.action(ArgAction::Set),
)
.arg(
Arg::new("drop_output_ports")
.long("drop-output-ports")
.help("Comma-separated output port names to drop")
.required(false)
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("gv2block")
.about("Converts a gate-level netlist and Liberty proto to block IR")
.arg(
Arg::new("netlist")
.long("netlist")
.help("Input gate-level netlist (.gv, .v, or .gv.gz)")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("liberty_proto")
.long("liberty_proto")
.help("Input Liberty proto (.proto or .textproto)")
.required(true)
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("gv2ir")
.about("Converts a gate-level netlist and Liberty proto to XLS IR")
.arg(
Arg::new("netlist")
.long("netlist")
.help("Input gate-level netlist (.gv)")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("liberty_proto")
.long("liberty_proto")
.help("Input Liberty proto (.proto or .textproto)")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("collapse_sequential")
.long("collapse_sequential")
.value_name("BOOL")
.default_value("true")
.value_parser(clap::value_parser!(bool))
.help("If true, collapse sequential state variables by substituting next_state.")
.action(ArgAction::Set),
)
)
.subcommand(
clap::Command::new("gv2aig")
.about("Converts a gate-level netlist to AIGER, with or without a Liberty proto")
.arg(
Arg::new("netlist")
.long("netlist")
.help("Input gate-level netlist (.gv, .v, or .gv.gz)")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("liberty_proto")
.long("liberty_proto")
.help("Optional Liberty proto (.proto or .textproto). Omit this for assign-only structural netlists that use only ~, &, |, and ^.")
.action(ArgAction::Set),
)
.arg(
Arg::new("aiger_out")
.long("aiger-out")
.value_name("PATH")
.help("Path to write AIGER output; use .aag for ASCII or .aig for binary")
.required(true)
.action(ArgAction::Set),
)
.arg(
Arg::new("module_name")
.long("module_name")
.value_name("MODULE")
.help("Optional module name to select when netlist contains multiple modules")
.action(ArgAction::Set),
)
.arg(
Arg::new("collapse_sequential")
.long("collapse_sequential")
.value_name("BOOL")
.default_value("true")
.value_parser(clap::value_parser!(bool))
.help("If true, collapse sequential state variables by substituting next_state.")
.action(ArgAction::Set),
),
)
.subcommand(
clap::Command::new("gv-read-stats")
.about("Reads a gate-level netlist and prints summary statistics")
.arg(
clap::Arg::new("netlist")
.help("Input gate-level netlist (.gv or .gv.gz)")
.required(true)
.index(1),
),
)
.subcommand(
clap::Command::new("gv-dump-cone")
.about("Traverse the cone around a gate-level instance and emit CSV rows (instance_type,instance_name,traversal_pin,levels) to stdout")
.arg(
clap::Arg::new("netlist")
.help("Input gate-level netlist (.gv or .gv.gz)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("liberty_proto")
.long("liberty_proto")
.value_name("LIBERTY_PROTO")
.help("Liberty proto (.proto or .textproto) describing the cell library used by the netlist")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("module_name")
.long("module_name")
.value_name("MODULE")
.help("Optional module name to restrict the search; required when the netlist contains multiple modules"),
)
.arg(
clap::Arg::new("instance")
.long("instance")
.value_name("INSTANCE")
.help("Instance name at the cone center")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("start-pins")
.long("start-pins")
.value_name("CSV")
.help("Optional comma-separated list of starting pins on the instance; defaults to all input pins for --traverse=fanin and all output pins for --traverse=fanout")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("traverse")
.long("traverse")
.value_name("DIRECTION")
.help("Traversal direction from the instance: fanin or fanout")
.required(true)
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("dff_cells")
.long("dff_cells")
.value_name("CSV")
.help("Comma-separated list of DFF cell names that should act as stop boundaries when using --stop-at-dff")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("stop-at-levels")
.long("stop-at-levels")
.value_name("N")
.help("Stop traversal once instances beyond distance N from the start instance would be reached"),
)
.arg(
clap::Arg::new("stop-at-dff")
.long("stop-at-dff")
.help("Stop traversal at DFF-like cells inferred from the Liberty library; do not traverse beyond them")
.action(ArgAction::SetTrue),
)
.arg(
clap::Arg::new("stop-at-block-port")
.long("stop-at-block-port")
.help("Stop traversal at module ports; do not traverse beyond the block boundary")
.action(ArgAction::SetTrue),
),
)
.subcommand(
clap::Command::new("g8r2v")
.about("Converts a .g8r or .g8rbin file to a .ugv netlist on stdout, optionally adding a clock port as the first input.")
.arg(
clap::Arg::new("g8r_input_file")
.help("The input .g8r or .g8rbin file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("add-clk-port")
.long("add-clk-port")
.value_name("NAME")
.help("Name for the clock port. Mandatory if --flop-inputs or --flop-outputs is used. If specified without flopping, adds a clock port with this name.")
.required(false),
)
.arg(
clap::Arg::new("flop-inputs")
.long("flop-inputs")
.help("Add a layer of flops for all inputs.")
.action(clap::ArgAction::SetTrue),
)
.arg(
clap::Arg::new("flop-outputs")
.long("flop-outputs")
.help("Add a layer of flops for all outputs.")
.action(clap::ArgAction::SetTrue),
)
.arg(
clap::Arg::new("use-system-verilog")
.long("use-system-verilog")
.help("Emit SystemVerilog instead of Verilog.")
.action(clap::ArgAction::SetTrue),
)
.arg(
clap::Arg::new("module-name")
.long("module-name")
.value_name("MODULE_NAME")
.help("Name of the generated module"),
)
)
.subcommand(
clap::Command::new("aig2v")
.about("Converts an AIGER file to a gate-level netlist on stdout, optionally adding a clocked wrapper.")
.arg(
clap::Arg::new("aig_input_file")
.help("The input AIGER file (.aag or .aig)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("module-name")
.long("module-name")
.value_name("MODULE_NAME")
.help("Name of the generated module")
.required(true),
)
.arg(
clap::Arg::new("fn_type")
.long("fn-type")
.value_name("FN_TYPE")
.help("Optional explicit bits-only function type used to emit packed ports, e.g. '(bits[16], bits[16]) -> bits[16]'")
.required(false),
)
.arg(
clap::Arg::new("add-clk-port")
.long("add-clk-port")
.value_name("NAME")
.help("Name for the clock port. Mandatory if --flop-inputs or --flop-outputs is used. If specified without flopping, adds a clock port with this name.")
.required(false),
)
.arg(
clap::Arg::new("flop-inputs")
.long("flop-inputs")
.help("Add a layer of flops for all inputs.")
.action(clap::ArgAction::SetTrue),
)
.arg(
clap::Arg::new("flop-outputs")
.long("flop-outputs")
.help("Add a layer of flops for all outputs.")
.action(clap::ArgAction::SetTrue),
)
.arg(
clap::Arg::new("use-system-verilog")
.long("use-system-verilog")
.help("Emit SystemVerilog instead of Verilog.")
.action(clap::ArgAction::SetTrue),
)
)
.subcommand(
clap::Command::new("g8r-area-table")
.about("Reports live AIG AND-node area attribution per PIR node id from a .g8rbin with provenance.")
.arg(
clap::Arg::new("g8r_input_file")
.help("The input .g8rbin file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("ir_input_file")
.help("The input XLS IR file")
.required(true)
.index(2),
)
.arg(
clap::Arg::new("group_by_opcode")
.long("group-by-opcode")
.help("Group the attribution table by PIR opcode instead of PIR node id.")
.action(clap::ArgAction::SetTrue),
)
.add_ir_top_arg(false),
)
.subcommand(
clap::Command::new("g8r-critical-path-table")
.about("Reports PIR attribution for the live AIG AND nodes that lie on at least one max-level input-to-output path.")
.arg(
clap::Arg::new("g8r_input_file")
.help("The input .g8rbin file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("ir_input_file")
.help("The input XLS IR file")
.required(true)
.index(2),
)
.arg(
clap::Arg::new("group_by_opcode")
.long("group-by-opcode")
.help("Group the attribution table by PIR opcode instead of PIR node id.")
.action(clap::ArgAction::SetTrue),
)
.add_ir_top_arg(false),
)
.subcommand(
clap::Command::new("g8r2ir")
.about("Converts a .g8r or .g8rbin GateFn file to an XLS IR package on stdout.")
.arg(
clap::Arg::new("g8r_input_file")
.help("The input .g8r or .g8rbin file")
.required(true)
.index(1),
)
)
.subcommand(
clap::Command::new("g8r-equiv")
.about("Checks if two GateFns are equivalent by lifting them to IR")
.arg(
clap::Arg::new("lhs_g8r_file")
.help("The left-hand side GateFn file (.g8r or .g8rbin)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("rhs_g8r_file")
.help("The right-hand side GateFn file (.g8r or .g8rbin)")
.required(true)
.index(2),
)
.arg(
Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("g8r-ir-equiv")
.about("Checks if a GateFn and an IR are equivalent by lifting GateFn into IR")
.arg(
Arg::new("g8r_file")
.help("The GateFn file (.g8r or .g8rbin)")
.required(true)
.index(1),
)
.arg(
Arg::new("rhs_ir_file")
.help("The right-hand side IR file")
.required(true)
.index(2),
)
.add_ir_top_arg(false)
.arg(
Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(ArgAction::Set),
)
.add_bool_arg(
"flatten_aggregates",
"Flatten tuple and array types to bits for equivalence checking",
)
.arg(
Arg::new("drop_params")
.long("drop_params")
.help("Comma-separated list of parameter names to drop from both functions before equivalence checking")
.action(ArgAction::Set),
)
.arg(
Arg::new("parallelism_strategy")
.long("parallelism-strategy")
.value_name("STRATEGY")
.help("Parallelism strategy")
.value_parser(["single-threaded", "output-bits", "input-bit-split"])
.default_value("single-threaded")
.action(ArgAction::Set),
)
.arg(
Arg::new("assertion_semantics")
.long("assertion-semantics")
.value_name("SEMANTICS")
.help("Assertion semantics")
.value_parser(clap::value_parser!(AssertionSemantics))
.default_value("ignore")
.action(ArgAction::Set),
)
.arg(
Arg::new("assert_label_filter")
.long("assert-label-filter")
.value_name("REGEX")
.help("Include only assertions whose label matches this regex (use `|` to combine labels)")
.action(ArgAction::Set),
)
.add_bool_arg(
"lhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the LHS GateFn-lifted IR",
)
.add_bool_arg(
"rhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the RHS IR, useful when only LHS or RHS has implicit token",
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("aig2ir")
.about("Converts an AIGER file to an XLS IR package on stdout.")
.arg(
clap::Arg::new("aig_input_file")
.help("The input AIGER file (.aag or .aig)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("fn_type")
.long("fn-type")
.value_name("FN_TYPE")
.help("Required explicit function type used to interpret the raw AIGER interface before lifting")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("aig-eval")
.about("Evaluates an AIGER file with the provided argument tuple")
.arg(
clap::Arg::new("aig_file")
.help("The AIGER file (.aag or .aig)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("arg_tuple")
.help("Tuple of typed IR values for the function arguments")
.required(true)
.index(2),
)
.arg(
clap::Arg::new("fn_type")
.long("fn-type")
.value_name("FN_TYPE")
.help("Optional superimposed function type, e.g. '(bits[32], bits[32]) -> bits[32]'")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("aig-equiv")
.about("Checks if two AIGER files are equivalent by lifting them to IR")
.arg(
clap::Arg::new("lhs_aig_file")
.help("The left-hand side AIGER file (.aag)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("rhs_aig_file")
.help("The right-hand side AIGER file (.aag)")
.required(true)
.index(2),
)
.arg(
Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(ArgAction::Set),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("aig-ir-equiv")
.about("Checks if an AIGER and an IR are equivalent via RHS signature packing")
.long_about(
r#"Checks if an AIGER and an IR are equivalent by lifting AIGER into IR.
The RHS IR function type determines how raw AIGER inputs and outputs are
interpreted before lift. See docs/bit_blasted_output_ordering.md, section
"Bit-Blasted Contract"."#,
)
.arg(
Arg::new("aig_file")
.help("The AIGER file (.aag or .aig)")
.required(true)
.index(1),
)
.arg(
Arg::new("rhs_ir_file")
.help("The right-hand side IR file")
.required(true)
.index(2),
)
.add_ir_top_arg(false)
.arg(
Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking (requires --features=with-easy-smt)")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(ArgAction::Set),
)
.add_bool_arg(
"flatten_aggregates",
"Flatten tuple and array types to bits for equivalence checking",
)
.arg(
Arg::new("drop_params")
.long("drop_params")
.help("Comma-separated list of parameter names to drop from both functions before equivalence checking")
.action(ArgAction::Set),
)
.arg(
Arg::new("parallelism_strategy")
.long("parallelism-strategy")
.value_name("STRATEGY")
.help("Parallelism strategy")
.value_parser(["single-threaded", "output-bits", "input-bit-split"])
.default_value("single-threaded")
.action(ArgAction::Set),
)
.arg(
Arg::new("assertion_semantics")
.long("assertion-semantics")
.value_name("SEMANTICS")
.help("Assertion semantics")
.value_parser(clap::value_parser!(AssertionSemantics))
.default_value("ignore")
.action(ArgAction::Set),
)
.arg(
Arg::new("assert_label_filter")
.long("assert-label-filter")
.value_name("REGEX")
.help("Include only assertions whose label matches this regex (use `|` to combine labels)")
.action(ArgAction::Set),
)
.add_bool_arg(
"lhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the lifted AIGER LHS IR",
)
.add_bool_arg(
"rhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the RHS IR",
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("aig-stats")
.about("Reads an AIGER file and reports structural + logical-effort statistics")
.arg(
clap::Arg::new("aig_input_file")
.help("The input AIGER file (.aag or .aig)")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("compute_graph_logical_effort")
.long("compute-graph-logical-effort")
.value_name("BOOL")
.action(clap::ArgAction::Set)
.value_parser(["true", "false"])
.num_args(1)
.help("Compute the graph logical effort worst case delay"),
)
.arg(
clap::Arg::new("graph_logical_effort_beta1")
.long("graph-logical-effort-beta1")
.value_name("BETA1")
.help("Beta1 value for graph logical effort computation (default 1.0)")
.value_parser(clap::value_parser!(f64))
.default_value("1.0")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("graph_logical_effort_beta2")
.long("graph-logical-effort-beta2")
.value_name("BETA2")
.help("Beta2 value for graph logical effort computation (default 0.0)")
.value_parser(clap::value_parser!(f64))
.default_value("0.0")
.action(clap::ArgAction::Set),
)
.add_bool_arg("quiet", "Quiet mode")
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON summary to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-aig-sharing")
.about("Finds and proves PIR node bit correspondences to AIG node outputs")
.arg(
clap::Arg::new("pir_ir_file")
.help("PIR/XLS IR package file to analyze")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("aig_file")
.help("AIGER file (.aag or .aig) to compare against")
.required(true)
.index(2),
)
.add_ir_top_arg(false)
.arg(
clap::Arg::new("sample_count")
.long("samples")
.value_name("N")
.help("Number of random samples for candidate discovery (default 256)")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("sample_seed")
.long("seed")
.value_name("U64")
.help("RNG seed for candidate discovery (default 0)")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"exclude_structural_pir_nodes",
"Exclude structural PIR nodes (default true)",
)
.arg(
clap::Arg::new("max_proofs")
.long("max-proofs")
.value_name("N")
.help("Limit number of candidates to prove (0 = no limit)")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("gate_formal_backend")
.long("gate-formal-backend")
.value_name("BACKEND")
.help("Formal backend for gate-level proof steps (default: cadical)")
.value_parser(["cadical", "varisat", "z3", "ir"])
.default_value("cadical")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("print")
.long("print")
.value_name("N")
.help("Print the first N per-candidate proof results (default 0)")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("print_mappings")
.long("print-mappings")
.value_name("N")
.help("Print PIR nodes with proved bit mappings (default: no limit; 0 = no limit)")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("output_json")
.long("output-json")
.value_name("PATH")
.help("Write a JSON report with the proved correspondences to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-fn-autocov")
.about("Runs coverage-guided corpus growth for an IR function and writes interesting tuples to an .irvals file")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false)
.arg(
clap::Arg::new("corpus_file")
.long("corpus-file")
.value_name("CORPUS_FILE")
.help("Newline-delimited .irvals corpus file to append to")
.required(true)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("seed")
.long("seed")
.value_name("SEED")
.help("PRNG seed")
.value_parser(clap::value_parser!(u64))
.default_value("0")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_iters")
.long("max-iters")
.value_name("MAX_ITERS")
.help("Maximum number of candidates to evaluate (omit to run until interrupted)")
.value_parser(clap::value_parser!(u64))
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_corpus_len")
.long("max-corpus-len")
.value_name("MAX_CORPUS_LEN")
.help("Stop successfully once the replayed/seeded/discovered corpus reaches this size")
.value_parser(clap::value_parser!(usize))
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("progress_every")
.long("progress-every")
.value_name("N")
.help("Emit progress every N iterations (0 disables periodic progress lines)")
.value_parser(clap::value_parser!(u64))
.default_value("10000")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("threads")
.long("threads")
.value_name("THREADS")
.help("Number of worker threads to use for candidate evaluation")
.value_parser(clap::value_parser!(usize))
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("seed_two_hot_max_bits")
.long("seed-two-hot-max-bits")
.value_name("BITS")
.help("Upper bit-width bound for two-hot structured seeds")
.value_parser(clap::value_parser!(usize))
.default_value("4096")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("no_mux_space")
.long("no-mux-space")
.value_name("BOOL")
.help("Disable printing the full mux-space summary at startup")
.value_parser(["true", "false"])
.default_value("false")
.num_args(1)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("seed_structured")
.long("seed-structured")
.value_name("BOOL")
.help("Seed with structured patterns (all-zeros/ones/one-hot/two-hot)")
.value_parser(["true", "false"])
.default_value("true")
.num_args(1)
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-fn-eval")
.about("Interprets an IR function with the provided argument tuple")
.arg(
clap::Arg::new("ir_file")
.help("Path to the IR file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("entry_fn")
.help("Name of the function to invoke")
.required(true)
.index(2),
)
.arg(
clap::Arg::new("arg_tuple")
.help("Tuple of typed IR values for the function arguments")
.required(true)
.index(3),
)
)
.subcommand(
clap::Command::new("ir-fn-node-count")
.about("Prints the node count for an IR function (excluding the reserved Nil node)")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false),
)
.subcommand(
clap::Command::new("ir-fn-node-count-corpus")
.about("Prints '<path>: <node-count>' for all .ir files under a corpus directory")
.arg(
clap::Arg::new("corpus_dir")
.help("Root directory to recursively scan for .ir files")
.required(true)
.index(1),
)
.add_ir_top_arg(false)
.add_bool_arg(
"ignore-parse-errors",
"Whether to skip IR files that fail to parse/validate/top-select (default true)",
)
.arg(
clap::Arg::new("max-files")
.long("max-files")
.value_name("N")
.help("Optional cap on number of .ir files to process after sorting (0 means no cap)")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-fn-structural-hash")
.about("Prints a rename-insensitive structural hash for an IR function")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false)
.add_bool_arg("json", "Output in JSON format"),
)
.subcommand(
clap::Command::new("ir-fn-to-json")
.about("Emits the selected IR function as JSON (including PIR text)")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false),
)
.subcommand(
clap::Command::new("xls-ir-fn-to-z3-smtlib")
.about("Emits Z3 SMT-LIB text for a selected XLS IR function")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(true),
)
.subcommand(
clap::Command::new("ir-fn-cone-extract")
.about("Extracts the backward cone feeding a selected node down to primary inputs (function parameters)")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("sink")
.help("Sink node selector: node name (e.g. 'my_node') or id/text_id (e.g. '123' or 'and.123')")
.required(true)
.index(2),
)
.add_ir_top_arg(false)
.add_bool_arg(
"emit_pos_data",
"Whether to retain position metadata (pos=...) and file_number table in the extracted cone",
),
)
.subcommand(
clap::Command::new("ir-fn-mffcs")
.about("Extracts ranked MFFCs (maximal fanout-free cones) from an IR function and writes selected cones to an output directory")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false)
.arg(
clap::Arg::new("output_dir")
.long("output_dir")
.value_name("DIR")
.help("Directory to write extracted MFFC packages as ${sha256}.ir")
.required(true)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_mffcs")
.long("max_mffcs")
.value_name("N")
.help("Optional cap on emitted MFFCs after ranking (0 means no cap)")
.default_value("200")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("min_internal_non_literal")
.long("min_internal_non_literal")
.value_name("N")
.help("Minimum non-literal internal-node count required to keep a candidate")
.default_value("4")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_frontier_non_literal")
.long("max_frontier_non_literal")
.value_name("N")
.help("Optional cap on non-literal frontier size (0 means no cap)")
.default_value("0")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"emit_pos_data",
"Whether to retain position metadata (pos=...) and file_number table in emitted cones",
)
.arg(
clap::Arg::new("manifest_jsonl")
.long("manifest_jsonl")
.value_name("PATH")
.help("Optional path for JSONL manifest output (default: <output_dir>/manifest.jsonl)")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("ir-strip-pos-data")
.about("Reads an .ir file and emits the same IR with all position data removed (file table and pos= attributes)")
.arg(
clap::Arg::new("ir_file")
.help("Path to the IR file")
.required(true)
.index(1),
),
)
.subcommand(
clap::Command::new("ir-bool-cones")
.about("Extracts all k-feasible boolean cones (cuts with frontier <= K) feeding bits[1] nodes and writes them to an output directory")
.arg(
clap::Arg::new("ir_input_file")
.help("The input IR file")
.required(true)
.index(1),
)
.add_ir_top_arg(false)
.arg(
clap::Arg::new("k")
.long("k")
.value_name("N")
.help("Maximum frontier size (K) for cuts; literals do not count toward K; tuples/arrays count by shape (e.g. a 3-tuple leaf costs 3)")
.required(true)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("output_dir")
.long("output_dir")
.value_name("DIR")
.help("Directory to write extracted cone packages as ${sha256}.ir")
.required(true)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_cuts_per_node")
.long("max_cuts_per_node")
.value_name("N")
.help("Safety cap: maximum number of cuts retained per IR node during enumeration")
.default_value("2048")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("max_cones")
.long("max_cones")
.value_name("N")
.help("Optional cap: stop after emitting N cones (0 means no cap)")
.default_value("0")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"emit_pos_data",
"Whether to retain position metadata (pos=...) and file_number table in emitted cones",
)
.arg(
clap::Arg::new("manifest_jsonl")
.long("manifest_jsonl")
.value_name("PATH")
.help("Optional path for JSONL manifest output (default: <output_dir>/manifest.jsonl)")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("run-verilog-pipeline")
.about("Runs a SystemVerilog pipeline via iverilog with a single input value")
.long_about("Runs a SystemVerilog pipeline simulation using iverilog.\n\nUsage: xlsynth-driver run-verilog-pipeline <SV_PATH> [INPUT_VALUE]\n SV_PATH: Path to SystemVerilog file (or '-' for stdin)\n INPUT_VALUE: XLS IR typed value (e.g., 'bits[32]:5', 'tuple(bits[8]:1, bits[16]:2)')\n If not provided, zero values will be used and displayed.")
.arg(
Arg::new("input_valid_signal")
.long("input_valid_signal")
.value_name("NAME")
.help("Input-valid signal name"),
)
.arg(
Arg::new("output_valid_signal")
.long("output_valid_signal")
.value_name("NAME")
.help("Output-valid signal name"),
)
.arg(
Arg::new("reset")
.long("reset")
.value_name("NAME")
.help("Reset signal name"),
)
.add_bool_arg("reset_active_low", "Reset is active low")
.arg(
Arg::new("clk")
.long("clk")
.value_name("NAME")
.help("Clock signal name for the DUT (default 'clk')"),
)
.arg(
Arg::new("latency")
.long("latency")
.value_name("CYCLES")
.help("Latency in cycles (required if output_valid_signal is not provided)"),
)
.arg(
Arg::new("waves")
.long("waves")
.value_name("PATH")
.help("Write VCD dump to PATH"),
)
.arg(
Arg::new("sv_path")
.help("Path to SystemVerilog pipeline source (use '-' for stdin)")
.required(true)
.index(1),
)
.arg(
Arg::new("input_value")
.help("XLS IR typed value used as input (e.g., 'bits[32]:5', 'tuple(bits[8]:1, bits[16]:2)'). If not provided, zero values will be used.")
.required(false)
.index(2),
),
)
.subcommand(
clap::Command::new("prove-quickcheck")
.about("Prove that DSLX #[quickcheck] functions always return true")
.add_dslx_input_args(false)
.arg(
clap::Arg::new("tactic_json")
.long("tactic_json")
.value_name("PATH")
.help("Path to a tactic script as a JSON array of steps. When present, uses the tactic-based prover instead of direct QuickCheck proving.")
.conflicts_with("tactic_jsonl"),
)
.arg(
clap::Arg::new("tactic_jsonl")
.long("tactic_jsonl")
.value_name("PATH")
.help("Path to a tactic script as JSONL (one JSON object per line). When present, uses the tactic-based prover instead of direct QuickCheck proving.")
.conflicts_with("tactic_json"),
)
.arg(
clap::Arg::new("test_filter")
.long("test_filter")
.value_name("FILTER")
.help("Regular expression; prove only quickcheck functions whose name fully matches the pattern"),
)
.arg(
clap::Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Select solver backend")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("assertion_semantics")
.long("assertion-semantics")
.value_name("SEM")
.help("Assertion semantics")
.value_parser(clap::value_parser!(QuickCheckAssertionSemantics))
.default_value("never")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("assert_label_filter")
.long("assert-label-filter")
.value_name("REGEX")
.help("Include only assertions whose label matches this regex (use `|` to combine labels)")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("uf")
.long("uf")
.value_name("func_name:uf_name")
.help("Treat DSLX function as uninterpreted: format <func_name>:<uf_name> (repeatable). Functions sharing the same uf_name are assumed equivalent; assertions inside them are ignored.")
.action(clap::ArgAction::Append),
),
)
.subcommand(
clap::Command::new("prove-enum-in-bound")
.about("Prove that target functions receive in-bound enum arguments when invoked from a DSLX top")
.add_dslx_input_args(true)
.arg(
clap::Arg::new("target")
.long("target")
.value_name("FUNCTION")
.help("Target function whose enum parameters must remain in-bound (repeatable)")
.required(true)
.action(clap::ArgAction::Append),
)
.arg(
clap::Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Select solver backend")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
"toolchain",
])
.default_value("auto")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("prover")
.about("Run a prover plan with a process-based scheduler")
.arg(
clap::Arg::new("cores")
.long("cores")
.value_name("N")
.help("Maximum concurrent processes to run")
.default_value("1")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("plan_json_file")
.long("plan_json_file")
.value_name("PATH_OR_-")
.help("Path to ProverPlan JSON file or '-' for stdin")
.required(true)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the overall result to PATH as JSON {\"success\": <bool>}")
.action(clap::ArgAction::Set),
),
)
.subcommand(
clap::Command::new("dslx-equiv")
.about("Checks if two DSLX functions are equivalent")
.arg(
clap::Arg::new("lhs_dslx_file")
.help("The left-hand side DSLX file")
.required(true)
.index(1),
)
.arg(
clap::Arg::new("rhs_dslx_file")
.help("The right-hand side DSLX file")
.required(true)
.index(2),
)
.arg(
clap::Arg::new("tactic_json")
.long("tactic_json")
.value_name("PATH")
.help("Path to a tactic script as a JSON array of steps. When present, uses the tactic-based prover instead of direct equivalence.")
.conflicts_with("tactic_jsonl"),
)
.arg(
clap::Arg::new("tactic_jsonl")
.long("tactic_jsonl")
.value_name("PATH")
.help("Path to a tactic script as JSONL (one JSON object per line). When present, uses the tactic-based prover instead of direct equivalence.")
.conflicts_with("tactic_json"),
)
.arg(
clap::Arg::new("dslx_top")
.long("dslx_top")
.value_name("TOP")
.help("Shared top-level function name (applies to both LHS and RHS if provided)"),
)
.arg(
clap::Arg::new("lhs_dslx_top")
.long("lhs_dslx_top")
.value_name("LHS_TOP")
.help("Top-level function name for the LHS DSLX file"),
)
.arg(
clap::Arg::new("rhs_dslx_top")
.long("rhs_dslx_top")
.value_name("RHS_TOP")
.help("Top-level function name for the RHS DSLX file"),
)
.arg(
clap::Arg::new("dslx_path")
.long("dslx_path")
.value_name("DSLX_PATH_SEMI_SEPARATED")
.help("Semi-separated search paths for DSLX modules"),
)
.arg(
clap::Arg::new("dslx_stdlib_path")
.long("dslx_stdlib_path")
.value_name("DSLX_STDLIB_PATH")
.help("Path to the DSLX standard library"),
)
.add_bool_arg(
"type_inference_v2",
"Enable the experimental type-inference v2 algorithm (external toolchain only)",
)
.arg(
clap::Arg::new("solver")
.long("solver")
.value_name("SOLVER")
.help("Use the specified solver for equivalence checking")
.value_parser([
"auto",
#[cfg(feature = "has-easy-smt")]
"z3-binary",
#[cfg(feature = "has-easy-smt")]
"bitwuzla-binary",
#[cfg(feature = "has-easy-smt")]
"boolector-binary",
#[cfg(feature = "has-bitwuzla")]
"bitwuzla",
#[cfg(feature = "has-boolector")]
"boolector",
#[cfg(feature = "has-boolector")]
"boolector-legacy",
"toolchain",
])
.default_value("auto")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"flatten_aggregates",
"Flatten tuple and array types to bits for equivalence checking",
)
.arg(
clap::Arg::new("drop_params")
.long("drop_params")
.value_name("CSV")
.help("Comma-separated list of parameter names to drop prior to equivalence checking"),
)
.arg(
clap::Arg::new("parallelism_strategy")
.long("parallelism-strategy")
.value_name("STRATEGY")
.help("Parallelism strategy")
.value_parser(["single-threaded", "output-bits", "input-bit-split"])
.default_value("single-threaded")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("assertion_semantics")
.long("assertion-semantics")
.value_name("SEMANTICS")
.help("Assertion semantics")
.value_parser(["ignore", "never", "same", "assume", "implies"])
.default_value("ignore")
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("assert_label_filter")
.long("assert-label-filter")
.value_name("REGEX")
.help("Include only assertions whose label matches this regex (use `|` to combine labels)")
.action(clap::ArgAction::Set),
)
.add_bool_arg(
"lhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the LHS IR, useful when only LHS or RHS has implicit token",
)
.add_bool_arg(
"rhs_fixed_implicit_activation",
"Fix the implicit activation bit to true for the RHS IR, useful when only LHS or RHS has implicit token",
)
.add_bool_arg(
"assume-enum-in-bound",
"Constrain enum-typed parameters to their defined values during equivalence proving",
)
.arg(
clap::Arg::new("lhs_uf")
.long("lhs_uf")
.value_name("func_name:uf_name")
.help("Treat LHS DSLX function as uninterpreted: format <func_name>:<uf_name> (repeatable). Mappings to the same uf_name across sides are assumed equivalent; assertions inside them are ignored.")
.action(clap::ArgAction::Append),
)
.arg(
clap::Arg::new("rhs_uf")
.long("rhs_uf")
.value_name("func_name:uf_name")
.help("Treat RHS DSLX function as uninterpreted: format <func_name>:<uf_name> (repeatable). Mappings to the same uf_name across sides are assumed equivalent; assertions inside them are ignored.")
.action(clap::ArgAction::Append),
)
.arg(
clap::Arg::new("output_json")
.long("output_json")
.value_name("PATH")
.help("Write the JSON result to PATH")
.action(clap::ArgAction::Set),
)
)
.subcommand(
clap::Command::new("gv-instance-csv")
.about("Emit a .csv.gz file listing all instance_name,cell_type pairs in a gate-level netlist.")
.arg(
clap::Arg::new("input")
.long("input")
.value_name("INPUT_NETLIST")
.help("Path to the input gate-level netlist (text)")
.required(true)
.action(clap::ArgAction::Set),
)
.arg(
clap::Arg::new("output")
.long("output")
.value_name("OUTPUT_CSV_GZ")
.help("Path to output .csv.gz file")
.required(true)
.action(clap::ArgAction::Set),
)
)
;
#[cfg(feature = "unstable-dslx-specialize")]
{
cmd = cmd.subcommand(
clap::Command::new("dslx-specialize")
.about(
"Specialize parametric DSLX functions reachable from a top function within the current module",
)
.add_dslx_input_args(true),
);
}
let matches = cmd.get_matches();
let mut toml_path: Option<String> = matches
.get_one::<String>("toolchain")
.map(|s| s.to_string());
if toml_path.is_none() {
let cwd = std::env::current_dir().unwrap();
let cwd_toml_path = cwd.join("xlsynth-toolchain.toml");
if cwd_toml_path.exists() {
log::info!(
"Using xlsynth-toolchain.toml in current directory: {}",
cwd_toml_path.display()
);
toml_path = Some(cwd_toml_path.to_str().unwrap().to_string());
}
}
let toml_value: Option<toml::Value> = toml_path.map(|path| {
if !std::path::Path::new(&path).exists() {
report_cli_error_and_exit(
"toolchain toml file does not exist",
None,
vec![
("path", &path),
(
"working directory",
&std::env::current_dir().unwrap().display().to_string(),
),
],
);
}
let toml_str =
std::fs::read_to_string(path).expect("read toolchain toml file should succeed");
toml::from_str(&toml_str).expect("parse toolchain toml file should succeed")
});
let config = toml_value.map(|v| {
let toolchain_config = v.clone().try_into::<XlsynthToolchain>().expect(&format!(
"parse toolchain config should succeed; value: {}",
v
));
toolchain_config.toolchain
});
match matches.subcommand() {
Some(("gv-instance-csv", subm)) => {
if let Err(e) = gv_instance_csv::do_gv_instance_csv(subm) {
eprintln!("error in gv-instance-csv: {e}");
std::process::exit(1);
}
}
Some(("dslx2pipeline", subm)) => {
dslx2pipeline::handle_dslx2pipeline(subm, &config);
}
Some(("dslx-stitch-pipeline", subm)) => {
dslx_stitch_pipeline::handle_dslx_stitch_pipeline(subm, &config);
}
Some(("dslx2ir", subm)) => {
dslx2ir::handle_dslx2ir(subm, &config);
}
#[cfg(feature = "unstable-dslx-specialize")]
Some(("dslx-specialize", subm)) => {
dslx_specialize::handle_dslx_specialize(subm, &config);
}
Some(("ir2opt", subm)) => {
ir2opt::handle_ir2opt(subm, &config);
}
Some(("ir-inline", subm)) => {
ir_inline::handle_ir_inline(subm, &config);
}
Some(("ir-mcmc-opt", subm)) => {
ir_mcmc_opt::handle_ir_mcmc_opt(subm);
}
Some(("ir2pipeline", subm)) => {
ir2pipeline::handle_ir2pipeline(subm, &config);
}
Some(("dslx2sv-types", subm)) => {
dslx2sv_types::handle_dslx2sv_types(subm, &config);
}
Some(("dslx-fn-eval", subm)) => {
dslx_fn_eval::handle_dslx_fn_eval(subm, &config);
}
Some(("dslx-fn-prove-assertions", subm)) => {
dslx_fn_prove_assertions::handle_dslx_fn_prove_assertions(subm, &config);
}
Some(("dslx-show", subm)) => {
dslx_show::handle_dslx_show(subm, &config);
}
Some(("dslx-list-fns", subm)) => {
dslx_list_fns::handle_dslx_list_fns(subm, &config);
}
Some(("dslx-g8r-stats", subm)) => {
dslx_g8r_stats::handle_dslx_g8r_stats(subm, &config);
}
Some(("ir2delayinfo", subm)) => {
ir2delayinfo::handle_ir2delayinfo(subm, &config);
}
Some(("ir-equiv", subm)) => {
ir_equiv::handle_ir_equiv(subm, &config);
}
Some(("ir-equiv-blocks", subm)) => {
ir_equiv_blocks::handle_ir_equiv_blocks(subm, &config);
}
Some(("dslx-equiv", subm)) => {
dslx_equiv::handle_dslx_equiv(subm, &config);
}
Some(("ir-ged", subm)) => {
ir_ged::handle_ir_ged(subm, &config);
}
Some(("ir-fn-to-block", subm)) => {
ir_fn_to_block::handle_ir_fn_to_block(subm, &config);
}
Some(("ir-fn-to-dslx", subm)) => {
ir_fn_to_dslx::handle_ir_fn_to_dslx(subm, &config);
}
Some(("ir-structural-similarity", subm)) => {
ir_structural_similarity::handle_ir_structural_similarity(subm, &config);
}
Some(("ir-localized-eco", subm)) => {
ir_localized_eco::handle_ir_localized_eco(subm, &config);
}
Some(("ir-query", subm)) => {
ir_query::handle_ir_query(subm, &config);
}
Some(("ir-rewrite", subm)) => {
ir_rewrite::handle_ir_rewrite(subm, &config);
}
Some(("ir-query-corpus", subm)) => {
ir_query_corpus::handle_ir_query_corpus(subm, &config);
}
Some(("ir-op-histo-corpus", subm)) => {
ir_op_histo::handle_ir_op_histo_corpus(subm, &config);
}
Some(("ir-op-histo", subm)) => {
ir_op_histo::handle_ir_op_histo(subm, &config);
}
Some(("ir-round-trip", subm)) => {
ir_round_trip::handle_ir_round_trip(subm);
}
Some(("ir-annotate-ranges", subm)) => {
ir_annotate_ranges::handle_ir_annotate_ranges(subm, &config);
}
Some(("ir2gates", subm)) => {
ir2gates::handle_ir2gates(subm, &config);
}
Some(("ir2g8r", subm)) => {
ir2gates::handle_ir2g8r(subm, &config);
}
Some(("dslx2pipeline-eco", subm)) => {
dslx2pipeline_eco::handle_dslx2pipeline_eco(subm, &config);
}
Some(("lib2proto", subm)) => {
lib2proto::handle_lib2proto(subm);
}
Some(("lib-query", subm)) => {
lib_query::handle_lib_query(subm, &config);
}
Some(("block2fn", subm)) => {
block2fn::handle_block2fn(subm, &config);
}
Some(("gv2block", subm)) => {
gv2block::handle_gv2block(subm);
}
Some(("gv2ir", subm)) => {
gv2ir::handle_gv2ir(subm);
}
Some(("gv2aig", subm)) => {
gv2aig::handle_gv2aig(subm);
}
Some(("gv-read-stats", subm)) => {
gv_read_stats::handle_gv_read_stats(subm);
}
Some(("gv-dump-cone", subm)) => {
gv_dump_cone::handle_gv_dump_cone(subm);
}
Some(("g8r2v", subm)) => {
if let Err(e) = g8r2v::handle_g8r2v(subm) {
report_cli_error::report_cli_error_and_exit(&e, None, vec![]);
}
}
Some(("aig2v", subm)) => {
if let Err(e) = aig2v::handle_aig2v(subm) {
report_cli_error::report_cli_error_and_exit(&e, Some("aig2v"), vec![]);
}
}
Some(("g8r2ir", subm)) => {
g8r2ir::handle_g8r2ir(subm, &config);
}
Some(("g8r-area-table", subm)) => {
g8r_table::handle_g8r_area_table(subm, &config);
}
Some(("g8r-critical-path-table", subm)) => {
g8r_table::handle_g8r_critical_path_table(subm, &config);
}
Some(("g8r-equiv", subm)) => {
g8r_equiv::handle_g8r_equiv(subm, &config);
}
Some(("g8r-ir-equiv", subm)) => {
g8r_ir_equiv::handle_g8r_ir_equiv(subm, &config);
}
Some(("aig-equiv", subm)) => {
aig_equiv::handle_aig_equiv(subm, &config);
}
Some(("aig2ir", subm)) => {
aig2ir::handle_aig2ir(subm, &config);
}
Some(("aig-eval", subm)) => {
aig_eval::handle_aig_eval(subm, &config);
}
Some(("aig-ir-equiv", subm)) => {
aig_ir_equiv::handle_aig_ir_equiv(subm, &config);
}
Some(("aig-stats", subm)) => {
aig_stats::handle_aig_stats(subm, &config);
}
Some(("ir-aig-sharing", subm)) => {
ir_aig_sharing::handle_ir_aig_sharing(subm, &config);
}
Some(("run-verilog-pipeline", subm)) => {
run_verilog_pipeline::handle_run_verilog_pipeline(subm);
}
Some(("ir-strip-pos-data", subm)) => {
ir_strip_pos_data::handle_ir_strip_pos_data(subm, &config);
}
Some(("ir-bool-cones", subm)) => {
ir_bool_cones::handle_ir_bool_cones(subm, &config);
}
Some(("ir-diverse-samples", subm)) => {
if let Err(e) = ir_diverse_samples::handle_ir_diverse_samples(subm) {
eprintln!("error in ir-diverse-samples: {e}");
std::process::exit(1);
}
}
Some(("ir-fn-autocov", subm)) => {
ir_fn_autocov::handle_ir_fn_autocov(subm, &config);
}
Some(("ir-fn-eval", subm)) => {
ir_fn_eval::handle_ir_fn_eval(subm, &config);
}
Some(("ir-fn-node-count", subm)) => {
ir_fn_node_count::handle_ir_fn_node_count(subm, &config);
}
Some(("ir-fn-node-count-corpus", subm)) => {
ir_fn_node_count_corpus::handle_ir_fn_node_count_corpus(subm, &config);
}
Some(("ir-fn-structural-hash", subm)) => {
ir_fn_structural_hash::handle_ir_fn_structural_hash(subm, &config);
}
Some(("ir-fn-to-json", subm)) => {
ir_fn_to_json::handle_ir_fn_to_json(subm, &config);
}
Some(("xls-ir-fn-to-z3-smtlib", subm)) => {
ir_fn_to_z3_smtlib::handle_ir_fn_to_z3_smtlib(subm, &config);
}
Some(("ir-fn-cone-extract", subm)) => {
ir_fn_cone_extract::handle_ir_fn_cone_extract(subm, &config);
}
Some(("ir-fn-mffcs", subm)) => {
ir_fn_mffcs::handle_ir_fn_mffcs(subm, &config);
}
Some(("prove-quickcheck", subm)) => {
prove_quickcheck::handle_prove_quickcheck(subm, &config);
}
Some(("prove-enum-in-bound", subm)) => {
prove_enum_in_bound::handle_prove_enum_in_bound(subm, &config);
}
Some(("prover", subm)) => {
prover::handle_prover(subm, &config);
}
Some(("ir2combo", subm)) => {
ir2combo::handle_ir2combo(subm, &config);
}
Some(("version", _)) => {
println!("{}", env!("CARGO_PKG_VERSION"));
}
_ => {
report_cli_error_and_exit("No valid subcommand provided.", None, vec![]);
}
}
}