Hardware Reference
In-Depth Information
Chapter 21
Formal Verification and Models
Hope is a great falsifier. Let good judgment keep her in check.
—
Baltasar Gracian
The scope of this topic does not admit detailed explanation of formal verification
algorithms. Instead, we provide hints about the way formal verification is conducted
and explain how assertions are interpreted in formal verification (FV). The material
in this chapter is primarily useful to people who deal with formal verification.
If you are interested in assertion simulation only you may skip the chapter, but we
recommended to read the chapter if you want to obtain a deeper understanding of
SystemVerilog assertions.
The DUT is represented as a set of states and a set of transitions between these
states. In FV, all DUT transitions are synchronized by the
global clock
, which is
the fastest clock in the particular part of the design hierarchy. See discussion about
possible multiple global clocks within a design in Sect.
4.4.2
. All other clocks are
synchronized with it.
Throughout this chapter, we make the following assumptions unless otherwise
stated:
We use the following conventions: the letters
a
,
b
, and
e
designate Boolean
expressions; the letters
r
and
s
designate sequences; and the letters
p
and
q
designate properties.
We freely switch between the abstract research notation and SystemVerilog
notation depending on the context. For example, when explaining theoretical
background we denote the disjunction of Boolean variables as a
_
b. Illustrating
the same formula in SystemVerilog, we write it as
a||b
. Analogously, in
the research notation we use
:
for negation (Boolean NOT),
^
for conjunction
(Boolean AND),
!
for implication, and
˚
for exclusive disjunction (modulo two
addition, or XOR).
Search WWH ::
Custom Search