Full Hardware Verification Pipeline

This release completes the hardware verification pipeline from English specifications through RTL linking to formal equivalence checking.

FOL-to-SVA Synthesis

Pattern-matching translation from first-order logic to SystemVerilog Assertions via Kripke-lowered structures, mapping quantified temporal patterns directly to SVA temporal operators.

Specification Analysis

Three new analysis modules assess specification quality before verification: coverage analysis measures how well SVA properties cover the spec knowledge graph, sufficiency analysis detects lonely signals and missing handshake patterns, and spec health checking catches contradictions and vacuity through the Z3 pipeline.

RTL Integration

A Verilog declaration parser extracts module structure (ports, signals, parameters, clock detection), and the RTL knowledge graph links spec-level and RTL-level signal names for automated property binding.

CEGAR Refinement & Decomposition

Counterexample-guided refinement classifies SVA divergence and suggests transformations. Hierarchical property decomposition enables independent verification of sub-properties.

Protocol Templates & Invariant Discovery

Pre-verified parameterizable SVA properties for AXI4, APB, and handshake protocols. Automatic candidate invariant generation from knowledge graph structure with Z3 verification.

Waveform & Consistency

Z3 counterexamples render to VCD format for waveform viewer inspection. Multi-property consistency checking with minimal unsatisfiable subset extraction.