xlsynth-driver 0.42.0

Binary that integrates XLS capabilities into a driver program
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

// SPDX-License-Identifier: Apache-2.0

use std::path::Path;

use crate::gate_ir_equiv::prove_gate_fns_equiv_via_ir;
use crate::ir_equiv::emit_equiv_outcome_and_exit;
use crate::toolchain_config::ToolchainConfig;
use xlsynth_g8r::aig::GateFn;
use xlsynth_g8r::aig_serdes::load_aiger_auto::load_aiger_auto_from_path;
use xlsynth_g8r::gate_builder::GateBuilderOptions;
use xlsynth_prover::prover::SolverChoice;

fn load_aig_gate_fn(path: &Path) -> Result<GateFn, String> {
    load_aiger_auto_from_path(path, GateBuilderOptions::no_opt())
        .map(|res| res.gate_fn)
        .map_err(|e| format!("failed to load {}: {}", path.display(), e))
}

fn gate_fn_signature_summary(g: &GateFn) -> String {
    let inputs = g
        .inputs
        .iter()
        .map(|i| format!("{}:bits[{}]", i.name, i.get_bit_count()))
        .collect::<Vec<String>>()
        .join(", ");
    let outputs = g
        .outputs
        .iter()
        .map(|o| format!("{}:bits[{}]", o.name, o.get_bit_count()))
        .collect::<Vec<String>>()
        .join(", ");
    format!("inputs=[{}] outputs=[{}]", inputs, outputs)
}

fn gate_fn_signatures_match(lhs: &GateFn, rhs: &GateFn) -> bool {
    if lhs.inputs.len() != rhs.inputs.len() {
        return false;
    }
    if lhs.outputs.len() != rhs.outputs.len() {
        return false;
    }
    if lhs
        .inputs
        .iter()
        .zip(rhs.inputs.iter())
        .any(|(a, b)| a.get_bit_count() != b.get_bit_count())
    {
        return false;
    }
    if lhs
        .outputs
        .iter()
        .zip(rhs.outputs.iter())
        .any(|(a, b)| a.get_bit_count() != b.get_bit_count())
    {
        return false;
    }
    true
}

pub fn handle_aig_equiv(matches: &clap::ArgMatches, config: &Option<ToolchainConfig>) {
    let lhs_path = Path::new(matches.get_one::<String>("lhs_aig_file").unwrap());
    let rhs_path = Path::new(matches.get_one::<String>("rhs_aig_file").unwrap());
    let solver: Option<SolverChoice> = matches
        .get_one::<String>("solver")
        .map(|s| s.parse().unwrap());
    let output_json = matches.get_one::<String>("output_json");

    let lhs = match load_aig_gate_fn(lhs_path) {
        Ok(g) => g,
        Err(e) => {
            eprintln!("aig-equiv error: {}", e);
            std::process::exit(2);
        }
    };
    let rhs = match load_aig_gate_fn(rhs_path) {
        Ok(g) => g,
        Err(e) => {
            eprintln!("aig-equiv error: {}", e);
            std::process::exit(2);
        }
    };

    if !gate_fn_signatures_match(&lhs, &rhs) {
        eprintln!(
            "aig-equiv error: gate function signatures do not match\nlhs: {}\nrhs: {}",
            gate_fn_signature_summary(&lhs),
            gate_fn_signature_summary(&rhs)
        );
        std::process::exit(2);
    }

    let tool_path = config
        .as_ref()
        .and_then(|c| c.tool_path.as_deref())
        .map(Path::new);
    let outcome = match prove_gate_fns_equiv_via_ir(&lhs, &rhs, solver, tool_path, "aig-equiv") {
        Ok(outcome) => outcome,
        Err(e) => {
            eprintln!("aig-equiv error: {}", e);
            std::process::exit(2);
        }
    };
    emit_equiv_outcome_and_exit(&outcome, "aig-equiv", output_json);
}