Formal Verification: An Essential Toolkit for Modern VLSI Design, Second Edition presents practical approaches for design and validation, with hands-on advice to help working engineers integrate these techniques into their work. Formal Verification (FV) enables a designer to directly analyze and mathematically explore the quality or other aspects of a Register Transfer Level (RTL) design without using simulations. This can reduce time spent validating designs and more quickly reach a final design for manufacturing. Building on a basic knowledge of SystemVerilog, this book demystifies FV and presents the practical applications that are bringing it into mainstream design and validation processes.
Every chapter in the second edition has been updated to reflect evolving FV practices and advanced techniques. In addition, a new chapter, Formal Signoff on Real Projects, provides guidelines for implementing signoff quality FV, completely replacing some simulation tasks with significantly more productive FV methods. After reading this book, readers will be prepared to introduce FV in their organization to effectively deploy FV techniques that increase design and validation productivity.
Author(s): Erik Seligman, Tom Schubert, M. V. Achutha Kiran Kumar
Edition: 2
Publisher: Morgan Kaufmann
Year: 2023
Language: English
Pages: 424
City: Cambridge, MA
Tags: Electronic Circuits; Integrated Circuits; Circuits Design; Verilog; Computer Hardware Description Language
Front Cover
Formal Verification
Formal Verification An Essential Toolkit for Modern VLSI Design
Copyright
Contents
Foreword by Harry Foster
Foreword to 1st edition by Robert Bentley
Acknowledgments
1 - Formal verification: from dreams to reality
What is FV?
Why this book?
A motivating anecdote
FV: the next level of depth
Overall advantages of FV
General usage models for FV
FV for complete coverage
FV for bug hunting
FV for exploring designs
FV in real design flows
FV methods not discussed in this book
The emergence of practical FV
Early automated reasoning
Applications to computer science
Model checking becomes practical
The standardizing of assertions
Challenges in implementing FV
Fundamental limitations of mathematics
Complexity theory
The good news
Amplifying the power of formal
Getting the most out of this book
Practical tips from this chapter
Further reading
2 - Basic formal verification algorithms
Formal verification in the validation process
A simple vending machine example
Comparing models
Cones of influence
Formalizing operation definitions
Building truth tables intelligently
Adding sequential logic
Boolean algebra notation
Basic Boolean algebra laws
Comparing specifications
Binary decision diagrams
Computing a BDD for a circuit design
Model checking with BDDs
Boolean satisfiability
Bounded model checking
Solving the SAT problem
The Davis–Putnam SAT algorithm
The Davis–Logemann–Loveland SAT algorithm
Additional SAT algorithm improvements
Chapter summary
Further reading
3 - Introduction to SystemVerilog Assertions
Basic assertion concepts
A simple arbiter example
What are assertions?
What are assumptions?
What are cover properties?
Clarification on assertion statements
SVA assertion language basics
Immediate assertions
Writing immediate assertions
Complications of procedural code and motivation for assert final
Location in procedural blocks
Boolean building blocks
Concurrent assertion basics and clocking
Sampling and assertion clocking
Sampled value functions
Concurrent assertion clock edges
Concurrent assertion reset (disable) conditions
Setting default clock and reset
Sequences, properties, and concurrent assertions
Sequence syntax and examples
Using sequences instead of $rose/$fell
Property syntax and examples
Named sequences and properties
Assertions and implicit multithreading
The challenge of constants
Writing the properties
Planning properties at the specification phase
Embedded properties during RTL development
Validation-focused properties
Connecting the properties to your design
Summary
Practical tips from this chapter
Further reading
4 - Formal property verification
What is FPV?
Example for this chapter: combination lock
Bringing up a basic FPV environment
Compiling your RTL
Creating cover properties
Creating assumptions
Creating assertions
Clocks and resets
Running the verification
How is FPV different from simulation?
What types and sizes of models can be run?
How do we reach targeted behaviors?
Simulation
Formal property verification
What values are checked?
Simulation
Formal property verification
How do we constrain the model?
Simulation
Formal property verification
How are constraints on internal nodes handled?
Simulation
Formal property verification
What do we use for debug?
Simulation
Formal property verification
How long are typical traces?
Simulation
Formal property verification
Deciding where and how to run FPV
Motivations for running FPV
Using design exercise FPV
Using bug hunting FPV
Using signoff quality FPV
Using application-specific FPV
Summary
Practical tips from this chapter
Further reading
5 - Effective formal property verification for design exercise
Example for this chapter: traffic light controller
Creating a design exercise plan
Design exercise goals
Major properties for design exercise
Complexity staging plan
Exit criteria
Putting it all together
Setting up the design exercise FPV environment
Cover properties
Assumptions
Assertions
Clocks and resets
Sanity checks
Wiggling the design
The wiggling process
Wiggling stage 1: our first short waveform
Debugging another short waveform
Exploring more interesting behaviors
Answering some new questions
Proving the assertions
Removing simplifications and exploring more behaviors
Facing complexity issues
Summary
Practical tips from this chapter
Further reading
6 - Effective FPV for verification
Deciding on your FPV goals
Bug hunting FPV
Signoff quality FPV
Staging your FPV efforts
Example for this chapter: simple ALU
Understanding the design
Creating the FPV verification plan
FPV goals
Major properties for FPV
Cover properties
Assumptions
Assertions
Reference modeling and properties
Addressing complexity
Staging plan
Blackboxes
Structural reduction
Quality checks and exit criteria
Exit criteria
Putting it all together
Running bug hunting FPV
Initial cover properties
Extended wiggling
Expanding the cover properties
Removing simplifications and exploring more behaviors
Evolution to Signoff Quality FPV
Summary
Practical tips from this chapter
Further reading
7 - Formal property verification apps for specific problems
Reusable protocol verification
Basic design of the reusable property set
Property direction issues
Verifying property set consistency
Checking completeness
Dynamic verification compatibility
Unreachable coverage elimination
The role of assertions in UCE
Covergroups and other coverage types
Connectivity verification
Model build for connectivity
Specifying the connectivity
Possible connectivity FPV complications
Coverage for connectivity FPV
Control register verification
Specifying control register requirements
SVA assertions for control registers
Major challenges of control register verification
Postsilicon debug and reactive FPV
Challenges of postsilicon FPV
UNEARTH: a practical methodology for postsilicon FPV
UNEARTH step 1: understand the problem
UNEARTH step 2: nail down the formal property
UNEARTH step 3: environment build for FPV
UNEARTH step 4: assess reachability
Semiformal methods
UNEARTH step 5: regulate the constraints
UNEARTH step 6: tap details from simulation
UNEARTH step 7: harness the full power of FPV
Summary
Practical tips from this chapter
Further reading
8 - Formal equivalence verification
Types of equivalence to check
Combinational equivalence
Sequential equivalence
Transaction-based equivalence
FEV use cases
RTL to netlist FEV
Netlist to netlist FEV
RTL to RTL FEV
Parameterization
Timing fixes—logic redistribution
Timing fixes—critical path reduction
Pipeline optimizations
Chicken bit validation
Clock gating verification
Running FEV
Choosing the models
Which models to verify?
Cell libraries
Key point selection and mapping
Defining the mappings
State negation
State replication
Unreachable points
Delayed and conditional mappings
Debugging mapping failures
Assumptions and constraints
Clock gating and similar protocols
Removing some functionality
Scan (and other netlist-only feature) insertion
Debugging mismatches
Additional FEV challenges
State element optimizations
Conditional equivalence
Don't care space
Complexity
Summary
Practical tips from this chapter
Further reading
9 - Formal verification's greatest bloopers: the danger of false positives
Misuse of the SVA language
The missing semicolon
Assertion at both clock edges
Short-circuited function with assertion
Subtle effects of signal sampling
Liveness properties that are not alive
Wrongly assuming a sequence
Preventing SVA-related false positives
Vacuity issues
Misleading cover property with bad reset
Proven memory controller that failed simulation
Contradiction between assumption and constraint
The queue that never fills, because it never starts
Preventing vacuity: tool and user responsibility
Implicit or unstated assumptions
Libraries with implementation assumptions
Expectations for multiply-driven signals
Unreachable logic elements: needed or not?
Preventing misunderstandings
Division of labor
Loss of glue logic
Case-splitting with missing cases
Undoing temporary hacks
Safe division of labor
Summary
Practical tips from this chapter
Further reading
10 - Dealing with complexity
Design state and associated complexity
Example for this chapter: memory controller
Observing complexity issues
Simple techniques for convergence
Choosing the right battle
Clocks and resets
Engine tuning
Blackboxing
Parameters and size reduction
Case-splitting
Hard and soft case split
Property simplification
Boolean simplifications
Making liveness properties finite
Cut points
Blackboxes with holes
Incremental FEV
Helper assumptions … and not-so-helpful assumptions
Writing custom helper assumptions
Leveraging proven assertions
Do you have too many assumptions?
Generalizing analysis using free variables
Exploiting symmetry with rigid free variables
Other uses of free variables
Downsides of free variables
Abstraction models for complexity reduction
Counter abstraction
Sequence abstraction
Memory abstraction
Shadow models
Semiformal verification
Evading the complexity problem: design and verification working together
Summary
Practical tips from this chapter: summary
Further reading
11 - Formal signoff on real projects
Overall signoff methodology
Plan and architect
DUT divide and conquer
Reviewing the design flow
Choosing the apps
Defining the FPV details
Filling the holes
Contingency plans
FV in main design milestones
Apply and execute
Ensure regular progress
Be ready for reactive FV
Cover and regress
Code coverage
Cover properties
FV regression
Machine learning and regressions
Network and cloud runs
Late stage rechecks
Track and close
Quality of formal verification
Timeline tracking
When is verification complete?
Conclusions
Practical tips from this chapter
12 - Your new FV-aware lifestyle
Uses of FV
Design exercise
Bug hunting FPV
Signoff quality FV
Specialized FV using apps
Formal equivalence verification
Individual preparation to use FV
Getting a team started on FV
Setting proper expectations
Invest in champions
Gain buy-in at all levels
Properly tracking FV efforts
Developing effective infrastructure
Making your manager happy
ROI calculation
Bug complexity ranking
What do FVers really do?
Summary
Practical tips from this chapter
Further reading
Index
A
B
C
D
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Back Cover
