EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations
The dataset tests whether generated SystemVerilog assertions survive changes in RTL structure without changing behavior.
EquivSVA groups 120 behavior families, each with four equivalent RTL implementations, shared gold properties, controlled mutants, and formal-validation evidence. The paper says every final family passes a 17-job validation suite covering equivalence, proofs, reachability, mutant checks, and distinguishability. In a small Qwen2.5-Coder-7B-Instruct case study, 93 of 293 generated interface-only properties were formally sound, with soundness varying across equivalent implementations in 14 of 24 test families. ArXiv · AI/CL/LG's note
EquivSVA groups 120 behavior families, each with four equivalent RTL implementations, shared gold properties, controlled mutants, and formal-validation evidence. The paper says every final family passes a 17-job validation suite covering equivalence, proofs, reachability, mutant checks, and distinguishability. In a small Qwen2.5-Coder-7B-Instruct case study, 93 of 293 generated interface-only properties were formally sound, with soundness varying across equivalent implementations in 14 of 24 test families. ArXiv · AI/CL/LG's note
score 4