Hardware Reference
In-Depth Information
Clock
clk
ticks infinitely many times, and
p
holds in infinitely many ticks of the
clock.
t
Sometimes mixing weak and strong operators in the same property is unavoid-
able, as in the case of
always s_eventually
p
,or
s_eventually always
p
.
However, when there is no special reason to mix weak and strong operators,
it is more efficient and more intuitive to use operators of the same strength
in the property. For example, instead of
p
until s_nexttime
q
, use either
p
until nexttime
q
or
p
s_until s_nexttime
q
, depending on whether or
not it is important to prove that
q
eventually happens.
Do not mix weak and strong operators in the same property unless it is
unavoidable.
21.6
Embedded Assertions
Thus far we have considered the formal semantics of stand-alone assertions (i.e.,
concurrent assertions placed outside procedural code) and properties. In this section,
we discuss how embedding concurrent assertions in procedural code modifies their
formal semantics. The simulation semantics of embedded assertions is described in
Chap.
14
. In FV, the support of embedded assertions is restricted, but it covers most
cases of importance.
As explained in Chap.
5
, if an assertion is in the scope of an
initial
procedure,
it is monitored only once, and if it is in the scope of an
always
procedure, it
is monitored continuously. In other words, if an assertion or an assumption is
embedded in an
always
procedure, an outermost
always
property operator is
implicitly added to this assertion.
12
If an assertion or an assumption is placed in the scope of one or several
procedural conditional statements, such as
if
or
case
, in the FV model an implicit
suffix implication is added to this assertion with the overall condition in the
antecedent.
12
Example 21.31.
Consider the following code fragment:
always
@(
posedge
clk)
begin
:b1
if
(en)
begin
:b2
// ...
if
(cond)
begin
:b3
// ...
12
See Chap.
18
for the semantics of embedded coverage statements.
Search WWH ::
Custom Search