Skip to main content

prove_spec_sva_equivalence

logicaffeine_compile::codegen_sva::hw_pipeline

Function prove_spec_sva_equivalence 

Source 
pub fn prove_spec_sva_equivalence(
    spec_source: &str,
    sva_text: &str,
    bound: u32,
) -> Result<EquivalenceResult, HwError>
Expand description

End-to-end: an English spec and a candidate SVA string → certified semantic equivalence with our prover. The Z3-free counterpart of check_z3_equivalence: the same translators, our CDCL → RUP tiers instead of Z3.