Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement
NeuroAssertion is presented, a coverage-driven assertion generation framework that combines formal trace generation, syntax-guided synthesis (SyGuS), and an agent-inspired refinement process within a unified framework that delivers around 2X more assertions and about 2X higher mutation coverage than traditional assertion mining methods.
Zhiyuan Yan, Ziyue Zheng, Hongce Zhang
· 0 citations