Simulation is effective at finding many early bugs in a design. It can sometimes find safety violations and sometimes find deadlock but it cannot prove liveness.

Once the early, low-hanging bugs are fixed, formal proof can be more effective at finding the remainder. These tend to lurk in unusual corner cases, where particular alignment or conjunction of conditions is not handled correctly.

If a bug has a one in ten million chance of being found by simulation, then it will likely be missed, since fewer than that number clock cycles might typically be simulated in any run. However, given a clock frequency of just 10 MHz, the bug might show up in the real hardware in one second!

Simulation is generally easier to understand. Simulation gives
performance results. Simulation can give a golden output that
can be compared against a stored result to give a pass/fail result.
A large collection of golden outputs is normally built up
and the current version of the design is compared against
them every night to spot **regressions**.

Simulation **test coverage** is expressed as a percentage. Given
any set of simulations, only a certain subset of the states will be
entered. Only a certain subset of the possible state-to-state transitions
will be executed. Only a certain number of the disjuncts to the guard
to an IF statement may hold. Only a certain number of paths
through the block-structured behavioural RTL may be taken.

There are many ways of defining coverage: for instance do we have to know the reachable state space before defining the state space coverage, or can we use all possible states as the denominator in the fraction?

In general software, a common coverage metric is the percentage of lines of code that are executed.

Scaling of formal checking is a practical problem: today's tools certainly cannot check a complete SoC in one pass. An incremental approach based around individual sub-systems is needed.

(C) 2008-10, DJ Greaves, University of Cambridge, Computer Laboratory.