This book describes SystemVerilog Assertions (SVA), a powerful temporal
assertion language, and how it enables all of these verification improvements.
It explains the basics of assertion-based verification (ABV) as well as the
syntax and semantics of SVA. Language constructs are illustrated with both
simple examples and examples drawn from common ABV problems. It then
ties all of this together by illustrating ABV with an OCP Cache and model
checking with a FIFO.
The SVA language is used because of its powerful temporal constructs, its
IEEE standardization in P1800—SystemVerilog—and its wide industry
support. These attributes make it a very attractive choice for verification teams.
What’s in This Book? This text can be divided into two major parts:
• SVA language
• SVA applications
Chapters 1 though 6 cover the SVA language:
Chapter 1 provides an introduction to assertion-based verification by
discussing the evolution of verification languages from procedural
languages to temporal assertion languages. It also provides an introduction
to SVA.
Chapter 2 discusses Booleans and sequences, including temporal delays
and repetitions.
Chapter 3 illustrates sequence operations.
Chapter 4 discusses properties, property operations, and multiclocked
properties.
Chapter 5 discusses assertion layer directives, clock flow, and clock
resolution.
Chapter 6 ties together the constructs discussed in chapters 1 through 5
by illustrating common assertion problems and implementing assertions
for simple designs.
Chapters 7 through 9 cover SVA applications:
Chapter 7 discusses assertion-based verification strategies, including
where to add assertions, who writes assertions, assertion coding
guidelines, assertion template libraries, and interfacing testbenches to
assertions.
Chapter 8 implements assertion-based verification for an OCP Cache.
Chapter 9 provides a primer on formal model checking, including what it
is, how it works, and how to use it. It formally proves assertions for a FIFO.
Interesting Areas of the Book. The book is structured to cover the needs of
a wide range of people, and although we recommend reading the entire book,
it might be useful for some people to start off by reading just a few chapters.
- For engineers who are new to assertion-based verification, we suggest starting with chapters 1, 2, and 7.
- For engineers who are familiar with assertion-based verification with a template library and want to learn how to write custom assertions, we suggest starting with chapters 2 through 6.
- For verification engineers who are familiar with another temporal language, we recommend skimming chapters 2 through 5, and then reading chapters 6 and 8 to ramp up quickly on the SVA language.
- For engineers who are familiar with assertion-based verification but want to understand additional techniques, we recommend chapters 7 and 9.
- For engineers wanting to learn model checking techniques, we recommend chapter 9.
- For hardware and ASIC managers who want to understand and manage assertion-based verification, we recommend chapters 1, 7, and 9.
- We recommend that all readers go through chapters 8 and 9 once they have gained some experience in SVA and assertion-based verification, because these chapters tie the concepts of both together in real world verification environments for both simulation-based and model checking-based verification.
