Module synthesis 

Reactive Synthesis from LTL

Given an LTL specification over environment inputs and system outputs, synthesize a controller (finite-state machine) that satisfies the spec against all possible environment behaviors.

Pipeline: LTL → Büchi automaton → Strategy search → Circuit → SVA/Verilog

Structs

Circuit

A synthesized controller circuit.

CircuitTransition

A single transition in the synthesized circuit.

SignalDecl

Signal declaration for synthesis.

Enums

SynthesisResult

Result of reactive synthesis.

Functions

circuit_to_sva

Generate SVA monitor from a synthesized circuit.

circuit_to_verilog

Generate Verilog RTL from a synthesized circuit.

synthesize_from_ltl

Synthesize a controller from an LTL specification.