022 · 断言被证明后,谁证明它值得验证?
ProofLoop 让 Agent 查询 RTL 结构并利用形式反例修正 SVA,显著提高可证明断言的比例;但在 Design2SVA 中,性质成立、性质非空洞与性质重要仍是三个不同判断。
ProofLoop 让 Agent 查询 RTL 结构并利用形式反例修正 SVA,显著提高可证明断言的比例;但在 Design2SVA 中,性质成立、性质非空洞与性质重要仍是三个不同判断。
ChipMEM 只把通过 EDA 验证的轨迹提炼为程序性记忆,并用工具调用统计指导重试;实验显示它能改善部分 RTL 优化和未见测试平台任务,但迁移证据仍受样本量与单次评测限制。