Hardware Reference
In-Depth Information
Unfortunately, it is not always possible formally to verify assumptions as
assertions on another block:
￿ the other block may be more complex,
￿ the drivers of the signals participating in the assumption may belong to different
blocks which then must be taken together, thus increasing the complexity of the
model,
￿ the signals in the assumptions may be generated by an Intellectual Property (IP)
block, etc.
In all these cases, the assumptions should at least be checked in simulation.
Furthermore, the assumptions should also be checked in simulation of larger models
in which the design is integrated.
20.6
Formal Verification Efficiency
For any FV flow, and especially for exhaustive verification, the quality of assertions
is critical. If in simulation inefficient assertions increase the simulation time, in
FV assertion efficiency may be a question of life and death: an FV session with
an inefficient assertion may not produce a conclusive result. Of course, assertion
efficiency in FV, as in simulation, is a matter of specific algorithms and tools, but
there are common principles that should be understood in order to write efficient
assertions.
Unfortunately, the requirements for assertion efficiency imposed by simulation
and FV are often different, sometimes even contradictory. The good news is that in
many cases a reasonable compromise can be found. When no compromise exists,
one should go after intended assertion usage—simulation or FV. If an assertion is
targeted for both modes, then efficiency in FV should be preferred. In rare critical
cases the same assertion can have different implementations for simulation and for
FV. These cases should be avoided whenever possible because it may be difficult to
ensure assertion equivalence.
The assertion efficiency requirements in emulation are usually more aligned with
FV than with simulation since both emulation and FV require assertion synthesis,
while assertion simulation algorithms may be implemented in a different way that
does not require synthesis. Note, however, that assertions synthesized for FV can be
nondeterministic, while for emulation they must be deterministic.
20.7
Hybrid Verification
There exist also hybrid methods combining simulation and FV for checking
assertions. These methods provide better coverage than simulation but are less
exhaustive than FV. The methods can usually handle much bigger designs than
Search WWH ::




Custom Search