022 · 断言被证明后，谁证明它值得验证？ProofLoop 让 Agent 查询 RTL 结构并利用形式反例修正 SVA，显著提高可证明断言的比例；但在 Design2SVA 中，性质成立、性质非空洞与性质重要仍是三个不同判断。