Hardware Reference
In-Depth Information
20.6.
What kinds of approximation do you know? When are they used? What kind
of approximation can result in false positives? In false negatives? What kind of
approximation is simulation?
20.7.
What kind of approximation is produced because of a missing assumption?
A redundant assumption?
20.8.
What result will be produced by FV in the case of contradictory assumptions?
In the case when an assumption contradicts the model?
20.9.
What is an empty model?
20.10.
What is pruning? Why is it used in FV?
20.11.
One of the additional pruning methods is
black-boxing
, in which a sub-
model is considered to be a black box. What kind of approximation is introduced by
black-boxing?
20.12.
What is the easiest way to debug specification correctness?
20.13.
Why are spurious counterexamples produced by FV tools? How can one
check whether a counterexample is spurious?
20.14.
What should be done if the FV result is inconclusive for an assertion?
20.15.
How can assumption correctness be checked?
20.16.
What is hybrid verification and when could it be used?
Search WWH ::
Custom Search