EquivSVA: A Formally Verified Dataset of Behavioral Assertions Across Equivalent RTL Implementations

Large language models are increasingly used to generate SystemVerilog Assertions from natural-language specifica- tions and register-transfer-level designs. Existing datasets and benchmarks support important goals such as large- scale training, formal evaluation, specification-to-assertion generatio