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

Solutions to bring the speed of simulation closer to that of the hardware being
simulated include hardware acceleration, emulation [ 39 ], and rapid prototyping.
In these methods, the design model is synthesized into a logic netlist, and this
netlist is mapped onto a Field-Programmable Gate Array (FPGA) or an equivalent
programmable device. Of course, checking a design in this way is still much
slower than running the real device, but it is significantly faster than simulation.
Because emulation tests are much longer than the simulation ones, they have a better
likelihood of revealing bugs that could not be reached in simulation. To capture these
bugs, assertions need also to be synthesized to become part of the emulation model.
In theory all SVA constructs are synthesizable, enabling the solution to work in most
cases. For some cases, however, this solution falls apart as some complex assertions
synthesize into enormous size, consuming a large amount of available gates.

1.4.3 Checking Assertions Using Formal Verification

Formal Verification (FV) [ 20 ] is the most powerful method to check design correct-
ness. It conducts exhaustive proof that the design complies with its specification.
More precisely, formal verification tools prove assertion correctness under the
hypothesis that all assumptions are satisfied. Unlike simulation and emulation, there
is no need to provide input stimuli. 8 If a tool can prove the assertion correctness, the
assertion is correct for any set of input stimuli under the specified assumptions.
The main limitation of FV methods is the capacity of FV tools. They can
handle only relatively small models, even though modern FV tools can efficiently
handle designs containing several thousands of state elements, latches and flip-
flops. Another important point to keep in mind is that the model for FV should
be completely specified, requiring all its input assumptions to be explicitly stated. If
some assumptions are missing, spurious assertion failures (so called false negatives )
may be reported, as discussed in Sect. 20.3 .
It follows that in simulation the main verification setup effort is modeling the
environment and devising the testbench, while in FV a great deal of effort is spent
on specifying assumptions.

8 Actually many verification tools do require some input information, such as a clock pattern or a
reset sequence.