Enum SynthesisResult 

pub enum SynthesisResult {
    Success {
        proof_term: Term,
        verilog: String,
        sva_properties: Vec<String>,
        iterations: u32,
    },
    Unrealizable(String),
    Failed(String),
}

Result of the synthesis pipeline.

Variants

Success

Successfully synthesized a circuit.

Fields

proof_term: Term

The kernel proof term (type-checked against the spec).

verilog: String

Extracted SystemVerilog.

sva_properties: Vec<String>

SVA properties for the synthesized circuit.

iterations: u32

Number of CEGAR iterations used.

Unrealizable(String)

The specification is unrealizable.

Failed(String)

Synthesis failed (timeout, unsupported, etc.)

Trait Implementations

impl Clone for SynthesisResult

fn clone(&self) -> SynthesisResult

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for SynthesisResult

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.