RV26 Todos
TODO: We need to review the paper and make sure we never use these terms interchangeably.
- There is only one instance of not solved being used along side falsified
- It is a footnote on pp. 4
- Right now, we mention that Not Proven encompasses both Falsified and Not Solved
- This was done so that we covered all possible FV results
- From our perspective the fact that they are not $\mathsf{Cat-1}$ was all we cared about.
- Another instance is pp. 15 where we say “the assertion is unverifiable in a reasonable amount of time”
TODO: I thought we were clear about this, but lets further highlight that our approach does not assume runtime-consistent assertions are necessarily valid invariants - and that we have an approach to ‘rollback’ falsified Cat-3s.
These are all the occurrences of the term $\mathsf{Cat}-3$
| pp. | |
|---|---|
| 5 | Caption |
| 6 | We explicitly say that they don’t have the same guarantees |
| 8 | Caption |
| 9 | We only talk about what the cardinality means |
| 9 | Maybe we can provide some rationale on why do convert them to assumptions |
| 11 | - |
| 12 | - |
| 13 | Expand |
| 14 | We explicitly say partial |
| 15 | Could be expanded |
The only “problematic” parts are pp. 9, 13 and 15
pp. 9
We first improve the coverage of both simulation and emulation workloads. After a desirable level of coverage is achieved, indicated by a reduction in the size of the appropriate categories, we attempt to close the FV-RV gap by utilizing two feedback strategies: First, we use consistent Cat-3 assertions to refine the RV workload, increasing its coverage.
How exactly does one go about refining? Do we see the CEX from FV and try to replicate that in RV? Do we stop at some point when we can no longer move Cat-3 to Cat-2?
We then convert Cat-3 assertions to assumptions to refine the FV environment.
This has to be rephrased. We may also need to add some rationale behind this.
With each future iteration, we confirm that these assertion-made-assumptions continue to be consistent with runtime workloads. Future RV iterations may falsify these assumptions, requiring tracking Cat-3 assertions that were used as assumptions.
Though we have said that they can be falsified, should we replace every instance on assumption with some other phrase such as quasi/pseudo/candidate-assumptions? Never referencing them as assumptions and always using this other phrase will remove any ambiguity.
TODO: We should also mention the possibility that even if Cat-3’s are falsified, they may allow deeper exploration of the design space and expose new bugs, and that this is an interesting area for future work.
This would be appropriate here
pp. 13
We subsequently imported these 52 Cat-3 global constant assertions as assump- tions into the JasperGold environment and re-ran formal verification on the more complex G(A →X(B)) assertions previously mined by HARM.
Should we move our experiments to fill in coverage gaps here? Because in the earlier sections we suggested performing this assertion-to-assumption conversion only when we are confident that there aren’t any holes.
pp. 15
Captions mention assumption instead of quasi/pseudo/candidate-assumption