Hardware Reference
In-Depth Information
If all states of the model are initial, i.e., I
D
Q, then this assumption is just an
invariant represented by the transition relation:
assume property
(R);
An assumption may be composed with a model, which is written as M
jj
q.This
composition defines the set of traces that are common for both M and q. In other
words, L.M
jj
q/
D
L.M /
\
L.q/. The assertion p is valid on the composition
M
jj
q, written as M
jj
q
ˆ
p,iffL.M
jj
q/
L.p/.
6
Example 21.15.
The assertion
always nexttime
o
is valid on the composition of
the module
m
from Example
21.8
and the assumption
always
!i
;
t
If assumption q and model M are contradictory, that is, there is no common
trace satisfying them, then L.M /
\
L.q/
D;
. In this case, M
jj
q
ˆ
p for any
assertion p. In this situation, the composite model M
jj
q is
empty
(Sect.
20.3.2
).
An empty composite model also results when several assumptions are contradictory.
It is a common mistake to think that formal verification fails when a model is empty,
in fact the opposite is true:
If a model is empty then formal verification declares success for any assertion.
Example 21.16.
Adding the assumption
always
i |=> o
to Example
21.8
, both
assertions
always
o |=> !o
and
always
i!=o
hold (as do any other assertions)
because the model is empty.
t
FV tools may report when an contradictory set of assumptions is detected. If
not, deploying coverage on some key properties of the design can provide useful
information.
21.3.3
Coverage
If a property p is used as an assertion, we verify its validity on a model M , that is,
every
trace accepted by M satisfies p. If we replace the requirement of validity by
the requirement of satisfiability, we obtain the notion of
coverage
(Sect.
4.7
).
We say that a property p is
satisfiable
, or that p is
covered
,onM if
there exists
a trace accepted by M that satisfies p. In other words, p is satisfiable, or covered,
on M iff L.M /
\
L.p/
¤;
. The notions of satisfiability and of validity are dual:
p is satisfiable on M iff M
6ˆ:
p.
6
In this case M
jj
q represents the so-called parallel composition of M and q and not the Verilog
Boolean OR.
Search WWH ::
Custom Search