342 hardware modules from the BasejumpSTL library are paired with formally-verified SystemVerilog Assertions generated and repaired by LLMs. Each module includes its RTL source, verified properties, full generation history, and formal verification scripts. The dataset, authored by Maohua Nie and hosted on Harvard Dataverse, was last updated in May 2026.
Use Cases
- Research on hierarchy-aware specification mining based on modules organized by depth from 0 to 9.
- Benchmarking automated property-mining tools based on the corpus of concurrent SVA properties.
- Curriculum-style training of assertion-generation models based on the LLM generation and repair history.
- Compositional verification research based on the dataset's organization into 8 functional groups.
Strengths
- 342 hardware modules provide a substantial corpus for analysis.
- Every property was mechanically checked end-to-end with formal verification (FPV, COV, FTA, FC).
- Includes full per-iteration LLM generation and repair history for traceability.
- Modules span 8 functional groups and hierarchy levels 0 through 9.
Limitations
- Column-level documentation is absent; field semantics must be inferred after download.
- Row count is unknown, which may limit suitability assessment.
Provenance
- Source
- Harvard Dataverse
- Collection Method
- LLM-generated assertions for modules from the open-source BasejumpSTL library.
- Time Range
- null
- Freshness
- Last updated 2026-05-06 22:51:37; freshness should be verified.
- Geography
- null