Procedural Assertions
In practice, most sequential
assertions are expressed as some form of implication, and thus require the
assertion writer to specify the antecedent expression to trigger the
assertion. As mentioned previously, one of the key advantages of unifying
assertions with the design language is to make it easier for the design
engineer to embed assertions in the design. However, declarative
assertions, by their very nature, often require additional work by the
designer to use them effectively.
Consider a finite state machine
design. Assertions in this type of design are often of the form �when in
this state, then that should happen,� such as �when in state
ACK, if foo is high, then req should be held low for 5 clocks.� This
assertion could be coded declaratively as:
P4: assert property(
@(posedge clk) (st == ACK) &&
(foo == 1) |-> !req[*5]);
Now, consider what the RTL code
would look like for the companion state machine:
always @(posedge clk)
case (st)
ACK:
if (foo == 1)
begin // when in this state, req should be low for 5 clocks
...
end
...
endcase |
It is interesting to note that
there are two specific pieces of information that are duplicated in the
design and the assertion: the clock and the trigger state. Instead of
requiring the designer to duplicate this information, the fact that the
assertions are syntactically part of the design language allows them to be
embedded procedurally in the RTL code and automatically infer this
information from the usage, as in:
always @(posedge clk)
case (st)
ACK:
if (foo == 1)
begin
P5: assert property (!req[*5]);
...
end |
This procedural concurrent
assertion (P5) is defined to be semantically equivalent to the declarative
concurrent assertion (P4) above, but is much easier to use and maintain.
Procedurally embedded assertions use the sampled values of signals to
evaluate the inferred trigger condition, just as declarative assertions
do. The inferencing rules for the antecedent include both case and
if-else statements, allowing arbitrarily complex triggers to be
inferred for procedural assertions. The resulting advantage for procedural
assertions is simple maintenance. That is, if the finite state machine
code is modified, the triggering condition for the assertion is
automatically updated, whereas the user would have to modify the code
manually to update the trigger of the corresponding declarative assertion,
introducing the possibility that the assertion will no longer accurately
reflect the design.
Assertion and Testbench
Interaction
As stated previously, a
significant advantage of unifying assertions with the design and
verification language is the ability for the assertions to communicate
information to the testbench. In a standalone assertion language there is
no such communication mechanism. In SystemVerilog, the pass and fail
statements of an assertion may execute any procedural statement, allowing
the user to notify the testbench that a sequence occurred, update coverage
counters, or anything else that may contribute to the effectiveness of the
verification, including setting signal values, calling class object
methods, or even calling C code.
Consider a bus protocol that
includes the property �a new bus cycle may not start for 2 clock cycles
after an abort cycle occurs.� This property could be coded as:
property
wait_after_abort;
@(posedge clk) abort_cycle |=> !cycle_start[*2];
endproperty
P6: assert property
(wait_after_abort); |
When the abort_cycle
sequence is detected, the property dictates that the cycle_start signal
will be low for two clocks. The property P6 codifies this behavior, and
can be used as a monitor in simulation to check the behavior, or in a
formal tool to try to prove that the behavior will never occur.
However, if this property is
defining the behavior of a top-level interface, the testbench will be
generating the bus transactions that must conform to this behavior. The
verification engineer writing the testbench can reuse the assertion
information as a constraint to help ensure that the generated stimulus
does not violate the behavior. Such a testbench might look something like:
program
manual_stimulus_generator;
repeat(1000)
begin
generate_transaction(addr,data);
while(wait_cnt > 0)
@(posedge clk) wait_cnt--;
end
endprogram |
The wait_cnt counter is used to
specify the delay between bus transactions generated by the testbench. The
abort_cycle sequence can be used to set this counter by using a cover
directive:
cover property( abort_cycle
) wait_cnt = 2;
Using the cover directive
allows the abort_cycle sequence to be detected, without producing an error
if it is not. When the sequence is detected, the wait_cnt counter is set
to 2, causing the testbench to wait 2 cycles before generating the next
transaction. The scheduling semantics of SystemVerilog ensure that there
will not be a race condition between the execution of the pass statement
and the testbench, which could not be guaranteed if the assertion were in
a different language.
SystemVerilog includes the
ability to specify an explicit synchronous interface between the testbench
and the design. The clocking domain construct defines when the
testbench will sample and drive device-undertest (DUT) signals relative to
a clock. By default, the sampling of signals by the testbench is the same
as the sampling used by assertions, ensuring that the testbench has access
to the same values as the assertions. As mentioned previously, this not
only avoids race conditions between the testbench/assertions and the DUT,
but it also affords the testbench a �post-synthesis� view of the design
behavior, with race conditions resolved according to synthesis rules,
during pre-synthesis RTL verification.