Module fol_to_sva 

FOL → SVA Formal Synthesis

Pattern-matches Kripke-lowered FOL structures to synthesize SystemVerilog Assertions. The key patterns:

Kripke Pattern	SVA Output
∀w'(Accessible_Temporal → P(w'))	assert property(@(posedge clk) P)
∃w'(Reachable_Temporal ∧ P(w'))	cover property(s_eventually(P))
∀w'(Next_Temporal → P(w'))	nexttime(P)
User If: P → Q with worlds	P |-> Q
¬(P ∧ Q) with worlds	!(P && Q)

Structs

SynthesizedSva

Result of SVA synthesis from a specification.

Functions

synthesize_sva_from_spec

Synthesize an SVA property from an English specification.