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

1.4 Checking Assertions

This section introduces how assertions are checked in different verification

environments:
￿ Simulation.
￿ Emulation.
￿ Formal analysis.

1.4.1 Checking Assertions in Simulation

Simulation [ 61 ] is modeling the behavior on a sequence of input stimuli, called a
(simulation) test. Simulation is the most popular method for checking assertions.
All major SystemVerilog simulators, for example, VCS R , Questa R , and Incisive R ,

support SVA and can check assertions, assumptions, and cover statements.
Of course, in simulation it is only possible to check whether an assertion is
violated in a given test case. If it is violated, we find a problem. But the absence
of violation does not mean that the design is correct—the same assertion may be
violated in another test case, or it may even be violated later in simulation if the
same test case is extended.
Although in theory no reasonable number of test cases is sufficient
to exhaustively check correctness of real designs, in practice simulation with
coverage measurements does provide significant confidence in system correctness
if no assertion violations are detected.
Typical simulators can report not only assertion violations, but also individual
transaction completions. By a transaction, we mean an individual case of assertion
evaluation. Figure 1.9 illustrates transaction completions for the following assertion:
req_ack: assert property (@( posedge clk) req |-> ##[1:3] ack);
This assertion states that each request req receives an acknowledgment ack in one
to three clock cycles from the moment when req was asserted. Figure 1.9 shows two
transactions, trans1 and trans2 . Transaction trans1 starts at time 20 and completes
at time 40, while transaction trans2 starts at time 90 but does not complete before
the end of simulation. An incomplete transaction does not necessarily indicate a
correctness problem because, had simulation lasted longer, the transaction might
complete as expected. However, this situation requires further analysis. When
crafting tests (directed and random) it is desirable to leave no transactions pending
(incomplete). Time points where there are no pending transactions are called
quiescent points . Although it is a good practice to ensure that the simulation always
ends at quiescent points, in reality it is hard to attain such a state for all assertions
at the same quiescent point. In general, it is necessary to analyze incomplete
transactions for any unexpected behavior.