Module synthesis_refine 

CEGAR Refinement for SVA Synthesis

When synthesized SVA doesn’t match the spec, classify the divergence as too-strong or too-weak, apply transformations, and re-check.

Structs

RefinementResult

Refinement result.

Enums

Divergence

Classification of synthesis divergence.

Functions

classify_divergence

Classify whether an SVA is too strong or too weak relative to the spec.

strengthen_implication

Apply a strengthening transformation to an SVA body. Converts non-overlapping to overlapping (removes delay).

weaken_implication

Apply a weakening transformation to an SVA body. Converts overlapping implication to non-overlapping (adds delay).

weaken_to_eventual

Apply an eventual-response transformation. Converts immediate response to eventual.