— Concurrent
assertions are based on clock semantics and use sampled values of variables.
One of the goals of SystemVerilog assertions is to provide a common semantic
meaning for assertions so that they can be used to drive various design and
verification tools. Many tools, such as formal verification tools, evaluate
circuit descriptions using cycle-based semantics, which typically relies on a
clock signal or signals to drive the evaluation of the circuit. Any timing or
event behavior between clock edges is abstracted away. Concurrent assertions incorporate these
clock semantic semantics. While this approach generally simplifies the evaluation
of a circuit description, there are a number of scenarios under which this
cycle-based evaluation provides different behavior from the standard
event-based evaluation of SystemVerilog.
—
$fatal is a
run-time fatal, which shall terminate the simulation
with an error code. The first argument passed to $fatal shall
be consistent with the argument to $finish.
The clock expression that controls evaluation of a
sequence can be more complex than just a single signal name. An
expression Expressions such as (clk && gating_signal)
and and (clk iff gating_signal) could can be
used to represent a gated
clock. Other more complex expressions are possible. In However, in order to ensure
proper behavior of the system and conform as closely as possible to truly
cycle-based semantics, the signals in a clock expression must be glitch-free
and should only transition once at any simulation time.
Change
in Syntax 17-2 (changes in red and blue):
sequence_match_item
::=
variable_assignment operator_assignment
| inc_or_dec_expression
| subroutine_call
Change
in Syntax 17-2 (changes in red and blue):
expression_or_dist
::=
expression [ dist { { dist_list } } ]
A ## followed by a
number or range specifies the delay from the current cycle clock tick to the
beginning of the sequence that follows. The delay ##1 indicates that the beginning of the
sequence that follows is one clock tick later than the current cycle clock tick.
The delay ##0 indicates that the beginning of the
sequence that follows is at the same clock tick as the current cycle clock tick.
Formal arguments can be optionally specified. A formal
argument is untyped, and is used for syntactic
replacement of a name or an expression in the sequence.
A sequence is declared with optional formal arguments.
When a sequence is instantiated, actual arguments can be passed to the sequence.
The sequence gets expanded with the actual arguments by replacing the formal
arguments with the actual arguments. Semantic checks are performed to ensure
that the expanded sequence with the actual arguments is legal.
In this example, sequences s1 and s2 are evaluated on
successive posedge event events of clk.
The sequence s3 is evaluated on
successive negedge events of clk.
To use a named sequence as a sub-sequence of another sequence,
simply reference its name. The evaluation of a sequence that references a named
sequence is performed in the same way as if the named sequence was contained as
a lexical part of the referencing sequence, with the formal arguments of the named sequence replaced by the actual ones and
the remaining variables in the named sequence resolved according to the scope
of the declaration of the named sequence. An example is shown below:
If te1 and te2 are sampled expressions (not sequences), the sequence (te1 and te2) matches if te1 and te2 both
evaluate to be true.
If both of these sequences
match and (c ##1 d) does not match, then evaluation
of ts2 results in these two
matches.
Sequence match
items can be attached to the operand sequence of the first_match operator. The sequence
match items are placed within the same set of parentheses that encloses the
operand. Thus, for example, the local variable assignment x = e can be attached to the first match of seq via
first_match(seq, x = e)
which is
equivalent to
first_match((seq,
x = e))
See Sections 17.8 and 17.9 for discussion of sequence match items.
Note these
changes are extensive repositioning of existing text plus some new text.
2. Discussion of implication
belongs in Section 17.11 on properties, not in Section 17.7 on sequences.
Nesting
{\courierbold disable iff}
clauses, explicitly or through property instantiations, is not allowed.
This
allows for the following examples:
and
continuing up to, but not including, the old Section "17.11.1 Recursive
properties".
This
allows for the following examples:
to
The
following examples illustrate the property forms.
The
meaning of implications has already been discussed in 17.7.11.
to
The
meaning of implications will be discussed below in 17.11.1.
3. LRM discussion of finite
trace semantics.
Add
the following section after Section "17.11.3 Recursive properties":
17.11.4
Finite-length
versus infinite-length behavior
The formal semantics in Annex H defines whether a given property
holds on a given behavior. How the
outcome of this evaluation relates to the design depends on the behavior that
was analyzed. In dynamic verification only behaviors that are finite in length
are considered. In such a case, SystemVerilog
defines four levels of satisfaction of a property:
Holds strongly:
—
no bad
states have been seen
—
all
future obligations have been met
—
the
property will hold on any extension of the path
Holds (but does not hold strongly):
—
no bad
states have been seen
—
all
future obligations have been met
—
the
property may or may not hold on a given extension of the path
Pending:
—
no bad
states have been seen
—
future
obligations have not been met
—
the property
may or may not hold on a given extension of the path
Fails:
—
a bad
state has been seen
—
future
obligations may or may not have been met
—
the
property will not hold on any extension of the path
4. Check non-degeneracy
discussion in LRM text and Formal Semantics.
Add
the following section after Section "17.11.4 Finite-length versus infinite-length
behavior":
17.11.5 Non-degeneracy
It is possible to define sequences that can never be matched. For
example:
(1'b1) intersect(1'b1 ##1
1'b1)
It is also possible to define sequences that admit only empty
matches. For example:
1'b1[*0]
A sequence that admits no match or that admits only empty matches
is called degenerate. A sequence that admits at least one non-empty
match is called non-degenerate. A more precise definition of non-degeneracy
is given in Annex H.
The following restrictions apply:
1.
Any
sequence that is used as a property must be non-degenerate and must not admit
any empty match.
2.
Any
sequence that is used as the antecedent of an overlapping implication (|->)
must be non-degenerate.
3.
Any
sequence that is used as the antecedent of a non-overlapping implication (|=>)
must admit at least one match. Such a sequence can admit only empty matches.
The reason for these restrictions is that the use of degenerate
sequences the forbidden ways results in counterintuitive property semantics,
especially when the property is combined with a disable iff clause.
Change
in Syntax 17-14 (changes in red and blue):
sequence_match_item
::=
variable_assignment operator_assignment
| inc_or_dec_expression
| subroutine_call
An x X
and z Z value of a bit is
not counted towards the number of ones.
property_spec ::=
[clocking_event ]
[ disable iff (expression expression_or_dist) ] property_expr
property_expr ::=
sequence_expr
| ( property_expr )
| not property_expr
| property_expr
or property_expr
| property_expr
and property_expr
| sequence_expr |-> property_expr
| sequence_expr |=> property_expr
| if ( expression expression_or_dist ) property_expr [ else property_expr ]
| property_instance
| clocking_event property_expr
5) A property is an if...else if it has either the form
if
(expression expression_or_dist) property_expr1
or
the form
if
(expression expression_or_dist) property_expr1 else property_expr2
A property of the first form evaluates to true if and only if
either expression expression_or_dist evaluates to false or property_expr1
evaluates to true. A property of the second form evaluates to true if and
only if either expression expression_or_dist evaluates
to true and property_expr1 evaluates to true or expression expression_or_dist evaluates to false and property_expr2
evaluates to true.
A disable iff clause can be attached to a property_expr
to yield a property_spec
disable iff (expression expression_or_dist) property_expr
property check_write_data_beat
(
expected_data, //
[0:127]
tag, // [3:0]
i // [3:0]
);
first_match first_match
(
##[0:$]
(
(data_valid && (data_valid_tag
== tag))
||
(retry && (retry_tag ==
tag))
)
)
|->
(
(
(data_valid && (data_valid_tag
== tag))
|->
(data == expected_data[i*8+:8])
)
and
(
if
(retry && (retry_tag == tag))
(
1’b1 |=> check_write_data_beat(tag, expected_data, 4’h0)
)
else
if (!last_data_valid)
(
1’b1 |=> check_write_data_beat(tag, expected_data, i+4’h1)
)
else
(
##1 (retry
&& (retry_tag == tag))
|=>
check_write_data_beat(tag, expected_data,
4’h0)
)
)
);
endproperty
In this example, source sequence e1 is evaluated at clock clk, while the destination
sequence e2 is
evaluated at clock sysclk. In e2, the end point of the
instance e1(ready,proc1,proc2) is tested to occur sometime after the
occurrence of inst. Notice that
method matched matched only tests for the end point of e1(ready,proc1,proc2) and has no bearing
on the starting point of e1(ready,proc1,proc2).
Local variables can be passed into an instance of a named sequence
to which matched matched is applied. The same restrictions apply as
in the case of ended ended. Values of local variables
sampled in an instance of a named sequence to which matched matched is applied will flow out under the same conditions as for ended ended. See Section
17.8.
As with ended ended, a
sequence instance to which matched matched is applied can have multiple
matches in a single cycle of the destination sequence clock. The multiple
matches are treated semantically the same way as matching both disjuncts of an or.
In other words, the thread evaluating the destination sequence will fork to
account for such
a1:assume property @(posedge clk) req dist
dist {0:=40, 1:=60} ;
always @(posedge clk) begin
<statements>;
assert property (rule);
end
bind_directive ::= // from Annex A.1.5
bind module_identifier bind_instantiation
;
| bind name_of_instance bind_instantiation ;
bind hierarchical_identifier constant_select bind_instantiation ;
The expect statement is a
procedural blocking statement that allows a property
to be declared and also to wait for the first successful match of the property
waiting on a property evaluation. The syntax of
the expect statement accepts a named property or a property declaration, and
is given below.
The expect statement accepts
the same syntax used to assert a property. An expect statement causes the executing process to block until the given
property successor succeeds or fails. The expect statement
unblocks at the earliest match of the property (i.e., first_match). The statement
following the expect is scheduled to execute after processing
the Observe region following the success of the
property, or the first failed attempt. In either case (i.e., in which the property completes its evaluation. When
the property succeeds or fails), the specified property
terminates its evaluation when the process unblocks, and the property stops being evaluated (i.e., no property
evaluation is started until that expect statement
is executed again).
When executed, the expect statement automatically
starts evaluating a single thread of
evaluation for the given property on the subsequent clocking event, that is, the
first attempt evaluation
shall take place on the next clocking event. When
the process unblocks (due to the property succeeding or failing) the property stops
being evaluated. If the property fails at
its clocking event, the optional else clause of the action block is executed. If the property succeeds
the optional pass statement of the action block is executed.
The semantics of the expect statement
are to block until first match (or failure) of the given property and whose
starting time is greater than the time at which the expect statement executes.
program tst;
initial begin
# 200ms;
expect( @(posedge clk) a ##1 b
##1 c ) else $error( "expect failed" );
ABC: ...
end
endprogram
In the above example, the expect statement blocks the specifies a property that consists of the sequence a ##1 b ##1 c. The expect statement
(second
statement in the initial block of program tst) blocks until the sequence a -> b -> c a ##1 b ##1 c is recognized starting with matched, or is determined not to match. The property evaluation starts on the following clocking event (posedge clk) after following the
200ms delay. If the sequence is matched at the corresponding time, the process is
unblocked and continues to execute on the statement labeled ABC. If the
sequence fails to match then the else clause is executed, which in this case
generates a run-time error. For the expect above to
succeed, the sequence a
-> b -> c a ##1 b ##1 c must match starting on the
clocking event (posedge clk) immediately after time 200ms. If a is false on the first clocking
event after 200ms, the expect fails. If a is
true on the first clocking event after 200ms and b is false one clocking event later,
the expect will also fail. The sequence
will not match if a, b, or c are
evaluated to be false at the first, second or third clocking event
respectively.
The expect statement can be incorporated
in any procedural code, including tasks or class methods. Because it is a
blocking statement, the property expression
can safely refer to automatic variables
as well as static variables. For example, the task below waits between 1 and 10
cycles clock ticks for the variable data data to have equal a particular value, which is an specified by the automatic argument value. The second
argument, success, is used to return
the result of the expect, expect statement: 1 for success and
0 for failure.