Skip to main content

synthesize_sva_from_spec

logicaffeine_compile::codegen_sva::fol_to_sva

Function synthesize_sva_from_spec 

Source 
pub fn synthesize_sva_from_spec(
    spec: &str,
    clock: &str,
) -> Result<SynthesizedSva, String>
Expand description

Synthesize an SVA property from an English specification.

Parses the spec, applies Kripke lowering, then pattern-matches the resulting FOL structure to produce SVA. The synthesized SVA uses the EXACT same signal names as the FOL translator so Z3 equivalence checking works.