Bitvector Theory & Bounded Model Checking

This release deepens the hardware verification pipeline with bitvector-level reasoning and temporal verification.

Bitvector & Array Types

The verification IR now supports BitVector(n) and Array(idx, elem) types with a full BitVecOp enum covering bitwise, shift, arithmetic, and comparison operations — all directly encodable to Z3's bitvector theory.

Bounded Model Checking

A new verify_temporal() method unrolls transition relations over bounded steps, checking temporal properties at each state and producing counterexamples on violation.

SVA Model Expansion

Seven new SVA expression variants — Repetition, SAlways, Stable, Changed, DisableIff, Nexttime, and IfElse — with parsing and emission support for richer assertion coverage.

Equivalence Checking

A new equivalence.rs module provides structural and semantic equivalence checking for verification expressions.