Hardware Reference
In-Depth Information
Assertion no_ack in Line 36 states that if upon sending the packet
( packet_sent ) there is no acknowledgment ( no_ack_thrice ), then the error
flag err should be asserted forever, that is, until the system reset occurs.
The above example shows that assertions can be inferred from a system level
description for expressing them in SVA. These assertions can then be applied to a
high level model in SystemVerilog and checked in simulation or proven formally.
Using SVA for system level has some difficulties. The main issue is clocks. The
system description is not always clock accurate, and is often formulated in terms
of transactions and real time. The signal activities are not expressed in terms of
transitions synchronized by design clocks. In contrast, SVA requires an exact clock
specification for every assertion. For example, the SVA specification in Fig. 1.6 is
less abstract than its verbal counterpart with respect to the specification of the clock,
reset, and timeout signals.
However, SVA has an important advantage that the same assertions may be used
directly or after some refinement as checkers in RTL verification, after the high level
model is refined to an RTL model of the design. As long as the high level model
embodies an approximate notion of a clock, it may still be possible to describe
assertions for the model. SVA provides several means for managing abstractions.
For example, we can define clock and reset only once using default clocking and
default disable iff statements. Specifying the exact clocks and resets requires
changing these statements only. The assertion building blocks are encapsulated in
let , sequence , and property statements. System refinement can thus be handled
using appropriate abstraction means. In our example, if the timeout mechanism
needs to be refined, it is enough to modify sequence no_ack_thrice . The mechan-
ics of attaching or substituting one model with another in the refinement process
is further supported by a configuration mechanism of SystemVerilog. 6 This is an
iterative step which continues to refine the architecture and to adjust the assertions
according to the modified requirements.
The situation gets more complicated if the language of the model is not
SystemVerilog. For example, high level models of Systems on Chip (SoCs) are often
written in SystemC, as this language can be natively integrated with the C/C CC
code of software components. Unfortunately, SystemC does not yet have its own
formal specification subset for assertions or provide a standard integration with
external formal specification languages [ 62 ]. Therefore, using SVA specifications
with SystemC models is tool dependent. There are other languages, such as
TLA [ 48 ] designed especially for high level system specification. These languages
are more abstract than SVA, and therefore better suited for this purpose. Detailed
discussion about high level model validation is out of the scope of this topic.
There are attempts in the academia and in the industry [ 21 , 55 , 68 ] to synthesize
an RTL model directly from its formal specification, and some promising results
have been demonstrated. Nevertheless, there is still a long way to go for this
approach to become practical, and we do not discuss it in this topic.
6 Configurations were introduced in Verilog 2001 [ 1 ].
Search WWH ::




Custom Search