Introduction - SVA: The Power of Assertions in SystemVerilog - page 6

The same intent may be expressed with a single assertion:
assert property (@( posedge clk) req |-> nexttime [4] grant);
Readers who are not yet convinced by this example can carry out Exercise 1.3 .
Assertions Formally Express Design Intent
SVA is a Formal Specification Language . It is used to describe design proper-
ties unambiguously and precisely. Usually properties are written as part of the high
level design specifications in a text document. But writing specification in a natural
language is ambiguous.
Consider the following typical property specification: Each request should be
granted in four clock cycles . This specification is ambiguous:
￿ Do we count four clock cycles starting from the cycle when the request was issued,
or from the next cycle?
￿ Do we require that the grant is issued during the first four cycles or exactly at the
fourth cycle?
￿ May two requests be served by the same grant or should they be served by two
separate grants?
The same specification written in SVA is unambiguous:
assert property (@( posedge clk) request |-> nexttime [4] grant);
This specification defines a clocked, or concurrent assertion, and it reads: when
request is issued, it should be followed by grant in the fourth clock cycle
measured from the clock cycle when request was issued.
Because of the formal nature of SVA, specifications can be interpreted by tools,
and what is more important, understood by humans. When the specifications are
formally defined, there is no place for misunderstanding.
Assertions Improve Bug Detection
Assertions promote systematic methodologies by tapping into several flexible ways
of inserting design checks. Once a methodology is set up to accommodate the needs
of a project and assertion libraries are established for the design style, the effort to
craft assertions becomes on par with writing ordinary code. The use of assertions
proliferates, within the design code and at the interfaces of design units, and thus
the design scrutiny is raised to trap errors. The checks remain in place from test
to test, without expending any additional effort. In a way, writing assertions turns
into something as simple as inserting comments. As a matter of course, bugs get
detected early and efficiently because of the widespread and comprehensive set of
assertion probes.