Module sva_to_verify 

SVA → Bounded Verification IR Translation

Translates SvaExpr to a bounded timestep model suitable for Z3 equivalence checking. Each signal at timestep t becomes a variable “signal@t”. Temporal operators are unrolled to bounded disjunctions/conjunctions.

Structs

DirectiveResult

Result of translating a directive — includes the semantic role.

SequenceMatch

A single match endpoint for a sequence expression.

SvaTranslator

Translator that converts SvaExpr to bounded timestep verification IR.

TranslateResult

Result of translating an SVA expression to bounded verification IR.

Enums

ArithBoundedOp

Arithmetic operations in bounded IR.

BitVecBoundedOp

Bitvector operations in bounded IR.

BoundedExpr

A verification expression in the bounded timestep model. This is a Z3-ready IR — each node maps directly to a Z3 AST construct.

BoundedSort

Sort annotation for bounded quantifiers.

CmpBoundedOp

Comparison operations in bounded IR.

DirectiveRole

The semantic role of a directive in formal verification.

Functions

collect_vars_from_bounded_pub

Public wrapper for collect_vars_from_bounded (for testing).

count_and_leaves

Count the number of And-leaves in a BoundedExpr tree.

count_or_leaves

Count the number of Or-leaves in a BoundedExpr tree.

extract_signal_names

Extract signal names from a BoundedExpr by collecting all Var names and stripping the @timestep suffix.