../

RV26 Actionable Items

Deadline for camera-ready version August 12

2 additional pages are available

Feedback

  • Conflation of falsified and not solved
    • Falsified provides more information that not-solved
  • $\mathsf{Cat-3}$ doesn’t mean anything. Just because it holds over finite traces doesn’t make that an invariant nor a valid assumption
    • This is true and a valid concern. We are never suggesting that it is a valid assumption rather it is a *reasonable assumption. The FPGA workloads are very extensive
  • Union-ing assertions causes trivially faulty assertions to be included and thus inflating the totals
    • This too is very valid. Right now we are just letting Jasper eliminate these
    • There isn’t really a proper way to solve this except . In order to scale we need to mine assertion parallelly
  • Cost of the Runtime Monitoring
    • This is an easy fix. Yasas can answer it
  • Reads like a case study
  • FPGA resource usage

Action Items

  • Differentiate falsified and not solved
  • Mention FPGA usage

Mentions of Falsified and Not Solved

  • Footnote on page 4
    • Right now, we mention that Not Proven encompasses both Falsified and Not Solved
    • We did this because from our perspective they are not $\mathsf{Cat-1}$, which was the initial categorization we required.
    • I think that is the only place we used Not Proven. We wanted to include this just for the sake of completeness but never thought it would become a thorn in our side

$\mathsf{Cat-3}$ being called valid in any sense

Pg. 6

Despite lacking the same guarantees as Cat-1 assertions, we still deem Cat-3 assertions useful for ABV and FV-RV gap analysis.

Pg. 9, Sec. 4

Has the assumption grid. We should add something to clearly indicate that these assumptions are not set in stone.

Pg. 13, Sec. 9

CVA-6 example. May be reiterate that these are not golden assumptions With the absence of no assumptions, what better assumptions can we make than RV consistent ones?