Module equivalence 

Semantic Equivalence Checking — The Core Contribution

The question nobody else asks: does the LLM-generated SVA express the SAME property as the formally parsed FOL?

Method

Given two VerifyExpr formulas (one from FOL, one from SVA), both unrolled to bounded timesteps:

1. Declare all signal@timestep variables as Z3 booleans
2. Construct ¬(FOL ↔ SVA)
3. If UNSAT → equivalent (no assignment makes them differ)
4. If SAT → extract counterexample trace from Z3 model
5. If UNKNOWN → timeout/undecidable

Why This Matters

Current industry practice: SVAs are checked against RTL (the hardware implementation). Nobody checks SVAs against the specification, because nobody has a formal specification. LOGOS provides one.

Structs

CycleState

Signal assignments at a single clock cycle.

EquivEncoder

Encoder that handles Bool, Int, BitVec, and Array Z3 expressions for equivalence checking.

Trace

A counterexample trace showing signal values at each clock cycle.

Enums

EquivalenceResult

Result of checking semantic equivalence.

SignalValue

Multi-sorted signal value for counterexample traces.

Functions

check_equivalence

Check whether two VerifyExpr formulas are semantically equivalent.

collect_int_vars_pub

Collect integer-typed variable names from a VerifyExpr (public API).

collect_quantifier_bound_vars_pub

Collect quantifier-bound variables from a VerifyExpr (public API).

collect_vars_pub

Collect all variable names referenced in a VerifyExpr (public API).

extract_signals

Extract unique signal names from a VerifyExpr by collecting Var references and stripping the @timestep suffix.