logicaffeine_compile/codegen_sva/
synthesis_refine.rs

1//! CEGAR Refinement for SVA Synthesis
2//!
3//! When synthesized SVA doesn't match the spec, classify the divergence
4//! as too-strong or too-weak, apply transformations, and re-check.
5
6use super::sva_model::SvaExpr;
7
8#[cfg(feature = "verification")]
9use super::hw_pipeline::check_z3_equivalence;
10
11/// Classification of synthesis divergence.
12#[derive(Debug, Clone, PartialEq)]
13pub enum Divergence {
14    /// SVA is stricter than the spec — it rejects valid behaviors.
15    TooStrong,
16    /// SVA is more permissive than the spec — it allows invalid behaviors.
17    TooWeak,
18    /// Cannot classify.
19    Unknown,
20}
21
22/// Refinement result.
23#[derive(Debug)]
24pub struct RefinementResult {
25    pub converged: bool,
26    pub iterations: u32,
27    pub final_sva: String,
28    pub divergence: Option<Divergence>,
29}
30
31/// Classify whether an SVA is too strong or too weak relative to the spec.
32///
33/// Too strong: spec allows a behavior that SVA rejects.
34/// Too weak: SVA allows a behavior that spec rejects.
35pub fn classify_divergence(
36    spec_allows_ce: bool,
37    sva_allows_ce: bool,
38) -> Divergence {
39    match (spec_allows_ce, sva_allows_ce) {
40        (true, false) => Divergence::TooStrong,
41        (false, true) => Divergence::TooWeak,
42        _ => Divergence::Unknown,
43    }
44}
45
46/// Apply a weakening transformation to an SVA body.
47/// Converts overlapping implication to non-overlapping (adds delay).
48pub fn weaken_implication(sva: &str) -> String {
49    sva.replace("|->", "|=>")
50}
51
52/// Apply a strengthening transformation to an SVA body.
53/// Converts non-overlapping to overlapping (removes delay).
54pub fn strengthen_implication(sva: &str) -> String {
55    sva.replace("|=>", "|->")
56}
57
58/// Apply an eventual-response transformation.
59/// Converts immediate response to eventual.
60pub fn weaken_to_eventual(sva: &str) -> String {
61    if sva.contains("|-> ") && !sva.contains("s_eventually") {
62        sva.replace("|-> ", "|-> s_eventually(") + ")"
63    } else {
64        sva.to_string()
65    }
66}
67
68/// Run a CEGAR refinement loop: check equivalence, classify divergence,
69/// apply transformation, re-check. Bounded to max_iterations.
70#[cfg(feature = "verification")]
71pub fn refine_sva(spec: &str, initial_sva: &str, clock: &str, bound: u32) -> RefinementResult {
72    use logicaffeine_verify::equivalence::EquivalenceResult;
73
74    let max_iterations: u32 = 5;
75    let mut current_sva = initial_sva.to_string();
76    let transformations: Vec<fn(&str) -> String> = vec![
77        weaken_implication,
78        strengthen_implication,
79        weaken_to_eventual,
80    ];
81
82    for i in 0..max_iterations {
83        let result = check_z3_equivalence(spec, &current_sva, bound);
84        match result {
85            Ok(EquivalenceResult::Equivalent) => {
86                return RefinementResult {
87                    converged: true,
88                    iterations: i + 1,
89                    final_sva: current_sva,
90                    divergence: None,
91                };
92            }
93            Ok(EquivalenceResult::NotEquivalent { .. }) => {
94                // Try next transformation
95                let transform_idx = i as usize % transformations.len();
96                let new_sva = transformations[transform_idx](&current_sva);
97                if new_sva == current_sva {
98                    // Transformation had no effect — try next one
99                    if transform_idx + 1 < transformations.len() {
100                        let alt_sva = transformations[transform_idx + 1](&current_sva);
101                        if alt_sva != current_sva {
102                            current_sva = alt_sva;
103                            continue;
104                        }
105                    }
106                    // No transformation helped
107                    return RefinementResult {
108                        converged: false,
109                        iterations: i + 1,
110                        final_sva: current_sva,
111                        divergence: Some(Divergence::Unknown),
112                    };
113                }
114                current_sva = new_sva;
115            }
116            Ok(EquivalenceResult::Unknown) | Err(_) => {
117                return RefinementResult {
118                    converged: false,
119                    iterations: i + 1,
120                    final_sva: current_sva,
121                    divergence: Some(Divergence::Unknown),
122                };
123            }
124        }
125    }
126
127    RefinementResult {
128        converged: false,
129        iterations: max_iterations,
130        final_sva: current_sva,
131        divergence: Some(Divergence::Unknown),
132    }
133}
logicaffeine_compile/codegen_sva/synthesis_refine.rs

logicaffeine_compile/codegen_sva/
synthesis_refine.rs
