SystemVerilog Language Overview - SVA: The Power of Assertions in SystemVerilog - page 38

Example 2.10. An assertion checking that both active_a and active_b are not
asserted together can be added to interface data from Example 2.9 :
interface data ( input logic clk);
logic [7:0] a, b;
logic active_a, active_b;
a_active: assert final (!(active_a && active_b))
else $error("a and b cannot be active simultaneously");
endinterface : data
Putting assertion a_active in interface data avoids its duplication if it were
put in the modules. In the latter case it should have been written twice: once as
an assertion in the module producer , and once as an assumption in the module
consumer . Of course, the same effect could be achieved by putting this assertion
in the module top . However, putting the assertion in the interface is preferable:
this assertion will be checked in the unit-level testing or formal verification of
component modules, and not only in the integration testing.

Discussion: Module consumer observes, but does not drive, the interface signals
active_a and active_b . Therefore, in formal verification of consumer it is
desirable to treat a_active as an assumption rather than as an obligation. Formal
verification tools generally treat assert statements as obligations and assume
statements as assumptions, but they also typically provide controls for overriding
the default interpretation. A tool may also provide an automatic mechanism for
characterizing an assertion based on its signal support, e.g. inferring that an assert
referencing only inputs be treated as an assumption rather than as an obligation. t

2.5 Programs

For writing testbenches SystemVerilog provides special design elements, called
programs . Their primary purpose is to generate and send stimuli to primary inputs
of a DUT and to receive its responses to validate the design behavior. A program is
similar to a module construct in its declaration of ports and body, but has a number
of limitations. For example, a program may contain continuous assignments,
initial and final procedures, but not always procedures. Programs may instantiate
checkers, but not other design elements (e.g., modules or other programs). The
main program feature distinguishing programs from modules is their simulation
semantics intended to avoid most races between the design and the testbench (see
Chap. 3 ). A detailed description of programs the reader can find in [ 59 ] and in
the LRM.

Example 2.11. We assume that the module router consumes request packets and
issues acknowledgment packets in the next clock cycle upon a request packet
reception. The test environment generating 100 request packets with random IDs
and random data is implemented by the program test .