../
Periscope Final Edits
Changes
Section 3.1
- These tools classify assertions as
+ We interpret the tools' classification as
As we later clarify that the tools’ original classification is proven, falsified and undetermined I felt that interpret should be used instead of saying that they tools themselves classify them as such.
- An assertion can be \emph{proven}, \emph{falsified}, or \emph{not solved}, but we combine the latter two into \emph{Not Proven} because these classes do not guarantee that assertions hold true for \emph{all} reachable states.
+ Formal tools deem assertions to be proven, falsified, or undetermined. We combine the latter two into Not Proven. Though they are distinct, from Periscope’s point of view, assertions without under-constrained guarantees are functionally the same, requiring further runtime confirmation.
This is the clarification that though distinct, for our use-case they are identical.
Section 4.5
- 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 \myclass{3} assertions to refine the RV workload, increasing its coverage.
+ Through this feedback, we first improve the coverage of both the simulation and emulation workloads. A coverage increase will be signified by the reduction in the size of the appropriate category: increased simulation coverage would reduce Cat-2 and increased runtime coverage would reduce Cat-3. Once this plateaus, we can attempt to close the FV-RV gap. This gap exists due to the lack of constraints in the formal environment. An easy heuristic to remedy this is to convert runtime consistent behavior into assumptions. We call these suppositions - to highlight that they are not formal assumptions , but rather temporary tools that aid the verification effort
- Removed improving coverage through consistent Cat-3 because it directly contradicted the first statement( After a desirable coverage is achieved… )
- Explicitly mention what each reduction means
- Use easy heuristic to characterize the weak nature of Cat-3 assumptions
- Introduce the word supposition
- From here on all occurrences of assumptions has been changed to suppositions
Non-Changes
- We discussed changing Section 3.3’s two categories to three i.e including Undetermined
- But this will require us changing the proceeding sentence too where we say distinguishing between these two …
- Here two refers to valid CEX and invalid CEX
- When we change it to three then this would become valid CEX, invalid CEX and undetermined.
- I don’t think undetermined is distinguished from the other two using RV
- Hence it is best to leave the paragraph as is. We already preface the section by saying assertions that fail…. Failing only have valid CEX and invalid CEX, hence it is semantically accurate.
- But this will require us changing the proceeding sentence too where we say distinguishing between these two …
- Section 4
- We agreed on not adding next text to explicitly say that the flow is cyclic
- This would have required us to explain exactly what is cyclic and what is not
- Causing substantial additional text
- Section 4.2
- Introducing Templates and the multiplicity of them
- We agreed not to do this because it would require defining what hierarchy meant and though we intuitively know what simple and complex mean, defining them rigorously would require too much text.