LLM-based generation of SystemVerilog Assertions (SVA) is often reported as nearing saturation, with the strongest specialized model reaching ${\sim}76\%$ accuracy on NL2SVA-Human. We show that this aggregate hides a temporal gap: models that appear strong overall still collapse to a few implication templates on bounded-delay and liveness specifications. The core issue is that the dominant recipe, supervised fine-tuning on NL/SVA pairs, optimizes token-level mimicry rather than the \emph{property equivalence} that defines SVA correctness. We introduce \emph{Reward-Weighted On-Policy Distillation} (RWOPD), an on-policy distillation method that samples student rollouts, scores them with an open SymbiYosys+Z3 Property-Equivalence Checker (PEC), and applies a verifier-reward-weighted forward-KL gradient from a frozen 14B teacher on verifier-passable rollouts. This keeps the supervision dense at every response token while grounding both selection and loss weight in property-equivalent behavior. RWOPD distills CodeV-SVA-14B into a Qwen2.5-Coder-7B-Instruct student that sets a new state of the art on NL2SVA-Human and NL2SVA-Machine across pass@1, pass@5, and pass@10, surpassing both specialized prior SOTA models and 671B general-purpose baselines.

翻译：基于大语言模型生成SystemVerilog断言（SVA）的技术常被报道趋于饱和，最强专用模型在NL2SVA-Human数据集上的准确率已达约76%。本文揭示该聚合指标掩盖了时间维度上的差距：表面表现优异的模型在处理有界延迟和活性规范时仍会退化为少数蕴涵模板。核心问题在于当前主流方法——基于NL/SVA对的监督微调——优化的是词元级模仿而非定义SVA正确性的“属性等价性”。我们提出“基于奖励的在线策略蒸馏”（RWOPD），该在线策略蒸馏方法采样学生模型生成结果，通过开源SymbiYosys+Z3属性等价性检查器（PEC）对其进行评分，并在通过验证器检验的生成结果上施加来自冻结14B教师模型的验证器奖励加权前向KL散度梯度。该方法在保持每个响应词元密集监督的同时，将选择与损失权重均锚定于属性等价行为。将CodeV-SVA-14B蒸馏至Qwen2.5-Coder-7B-Instruct学生模型后，RWOPD在NL2SVA-Human与NL2SVA-Machine数据集的pass@1、pass@5及pass@10指标上均创下新纪录，超越现有专用SOTA模型及671B通用基线模型。