A Roadmap for Formal Property Verification

By: Pallab Dasgupta

Write A Review

Hardcover | 5 July 2006

At a Glance

Hardcover
268 Pages

Dimensions(cm)
23.5 x 16.51 x 1.27

Hardcover

$169.00

or 4 interest-free payments of $42.25 with

Ships in 5 to 7 business days

Integrating formal property verification (FPV) into an existing design process raises several interesting questions. Have I written enough properties? Have I written a consistent set of properties? What should I do when the FPV tool runs into capacity issues? This book develops the answers to these questions and fits them into a roadmap for formal property verification - a roadmap that shows how to glue FPV technology into the traditional validation flow. A Roadmap for Formal Property Verification explores the key issues in this powerful technology through simple examples - you do not need any background on formal methods to read most parts of this book.

Industry Reviews

"This book is a "must-read" for anyone who needs a broad and deep understanding of assertion-based verification technology and methodology. It gives an in-depth overview of the logic behind, and algorithms for, reasoning about design behavior using assertions. The book also presents advanced methods for checking consistency and coverage of an assertion-based specification, for maintaining completeness of a specification as it is refined, and for leveraging assertions for automatic test generation in constrained random simulation.
Detailing both established practice and recent developments, "A Roadmap for Formal Property Verification" is a valuable reference for insight into both the present and the future of assertion-based verification." (Erich Marschner, Senior Architect, Systems and Functional Verification, Cadence Design Systems, and Co-Chair, Accellera Formal Verification Technical Committee (FVTC)

Shipping

	Standard Shipping	Express Shipping
Metro postcodes:	$9.99	$14.95
Regional postcodes:	$9.99	$14.95
Rural postcodes:	$9.99	$14.95

Orders over $79.00 qualify for free shipping.

How to return your order

At Booktopia, we offer hassle-free returns in accordance with our returns policy. If you wish to return an item, please get in touch with Booktopia Customer Care.

Additional postage charges may be applicable.

Defective items

If there is a problem with any of the items received for your order then the Booktopia Customer Care team is ready to assist you.

For more info please visit our Help Centre.

You Can Find This Book In

Non-Fiction Engineering & Technology Electronics & Communications Engineering Electronics Engineering Circuits & Components Computing & I.T.Computer Science Computer Architecture & Logic Design Mathematics Mathematical Foundation Mathematical Logic Technology in General

Engineering in General Energy Technology & Engineering Electrical Engineering Graphical & Digital Media Applications

Preface	p. xi
Introduction	p. 1
Writing Our First Formal Specification	p. 2
Is My Specification Correct?	p. 5
Have I written Enough Properties?	p. 6
Property Verification	p. 8
The Dynamic ABV Approach	p. 9
The FPV Approach	p. 11
Verification by Specification Refinement	p. 14
The New Flow	p. 17
Languages for Temporal Properties	p. 19
The Basic Temporal Operators	p. 22
Intuitive Explanation	p. 23
Formal Semantics	p. 24
Logics for Temporal Specification	p. 25
Linear Temporal Logic	p. 26
Computation Tree Logic	p. 27
LTL versus CTL	p. 29
Real Time Temporal Logics	p. 30
System Verilog Assertions	p. 31
A Quick Overview	p. 32
The Notion of Sequences	p. 37
Sequence Operations: Repetition	p. 38
Sequence Operations: And, Intersect, Or	p. 40
Local Variables	p. 41
Properties	p. 42
Assume-Assert Specifications	p. 44
The Cover Statement	p. 47
Architectural Styles for Assertion IPs	p. 47
The Main Steps	p. 49
Coding Styles: Event and State-based Checkers	p. 50
Concluding Remarks	p. 56
Bibliographic Notes	p. 57
How Does the Property Checker Work?	p. 59
Checkers are State Machines!	p. 61
The Verification Strategy	p. 63
Dynamic Property Verification	p. 64
Formal Property Verification	p. 67
Creating the Checker Automaton	p. 68
FSM Extraction	p. 72
Computing the Product	p. 74
BDD-based Formal Property Verification	p. 78
What is a BDD?	p. 79
BDDs for State Machines	p. 83
Symbolic Reachability	p. 84
CTL Model Checking	p. 90
SAT-based Formal Property Verification	p. 92
What is SAT?	p. 92
SAT-based Reachability	p. 93
Detecting Loops	p. 95
Unfolding Properties	p. 96
Bounded Model Checking	p. 96
Concluding Remarks	p. 97
Bibliographic Notes	p. 99
Is My Specification Consistent?	p. 101
Satisfiability and Vacuity	p. 103
Writing Unsatisfiable Specifications	p. 103
The Notion of Vacuity	p. 105
Satisfiability is not Enough	p. 105
Readability	p. 107
Receptiveness	p. 109
Games with the Environment	p. 114
Methods for Consistency Checking	p. 115
Alternating Automata and LTL	p. 117
Satisfiability Checks	p. 119
Realizability Checks	p. 121
Receptiveness Checks	p. 124
The SpecChecker Tool	p. 125
Concluding Remarks	p. 126
Bibliographic Notes	p. 128
Have I Written Enough Properties?	p. 129
Simulation Coverage Metrics	p. 131
Mutation-based FPV Coverage	p. 132
Falsity and Vacuity Coverage	p. 134
FSM Coverage	p. 135
Code and Circuit Coverage	p. 136
Structural Versus Functional Coverage	p. 136
Fault-based FPV Coverage	p. 138
The Coverage Strategy	p. 141
Coverage of Faults on Non-inputs	p. 142
Coverage of Faults on Inputs	p. 145
LTL-Covanalyzer: The Tool	p. 148
Building it Over FPV Tools	p. 149
Other Fault Models	p. 153
Concluding Remarks	p. 154
Bibliographic Notes	p. 155
Design Intent Coverage	p. 157
An Introductory Example	p. 160
Priority Cache Access: Architectural Specs	p. 160
Is my Implementation Plan Correct?	p. 162
The Correct Architecture	p. 165
How Does Design Intent Coverage Help?	p. 166
The Formal Problem	p. 167
Where is the Coverage Gap?	p. 171
How Should We Present the Coverage Hole?	p. 173
The Intent Coverage Algorithm	p. 174
Unfolding the Coverage Gap	p. 175
Elimination of Non-architectural Signals	p. 177
The Term Distribution Algorithm	p. 178
Weakening Unbounded Temporal Properties	p. 182
Special Treatment of Invariant Properties	p. 184
Soundness of the Intent Coverage Algorithm	p. 186
Multi-property Representation of the Coverage Gap	p. 186
SpecMatcher - The Intent Coverage Tool	p. 188
Priority Cache Access - A Closer Look	p. 189
Concluding Remarks	p. 192
Bibliographic Notes	p. 193
Test Generation Games	p. 195
Constrained Random Test Generation	p. 196
Layered Verification Methodologies	p. 197
The Benefits	p. 199
The Limitations	p. 201
Dynamic Coverage Driven Verification	p. 202
Assertions Viewed as Coverage Points!	p. 203
Games with the Environment	p. 204
Vacuity Games	p. 205
Readability Games	p. 207
Intelligent Test Generation for Property Coverage	p. 208
Dynamic Monitoring	p. 208
Online Test Generation	p. 209
Test Generation Algorithms	p. 210
The Integrated Verification Flow	p. 212
Concluding Remarks	p. 214
Bibliographic Notes	p. 215
A Roadmap for Formal Property Verification	p. 217
Simulation-based Validation Flow	p. 218
Formal Verification Flow	p. 221
The Three Pillars	p. 224
What's Between Simulation and Model Checking?	p. 229
What's between Intent Coverage and Model Checking?	p. 231
What's between Intent Coverage and Simulation?	p. 233
The Integrated Flow	p. 234
Architectural Validation	p. 235
RTL Validation	p. 236
Sharing the Task	p. 238
Architect's Corner	p. 238
Design Manager's Corner	p. 239
Unit Designer's Corner	p. 240
Concluding Remarks	p. 240
References	p. 243
Index	p. 249
Table of Contents provided by Ingram. All Rights Reserved.

A Roadmap for Formal Property Verification

At a Glance

Hardcover

Industry Reviews

Shipping

How to return your order

Defective items

You Can Find This Book In

More in Computer Architecture & Logic Design

Practical Approach to Open Source Intelligence (OSINT)

Volume 2

Parallel Computing

Design and Analysis of Algorithms

Computer Architecture

A Modern Approach

Basic Computer Architecture

Fundamentals of Software Architecture

A Modern Engineering Approach

Making Embedded Systems

2nd Edition - Design Patterns for Great Software

Architecture Patterns with Python

Enabling Test-Driven Development, Domain-Driven Design, and Event-Driven Microservices

Clean Architecture

A Craftsman's Guide to Software Structure and Design

The Software Architect Elevator

Redefining the Architect's Role in the Digital Enterprise

Developing Graphics Frameworks with Java and OpenGL

Rust Atomics and Locks

Low-Level Concurrency in Practice

Platform Engineering

A Guide for Technical, Product, and People Leaders

Learning Systems Thinking

Essential Non-Linear Skills and Practices for Software Professionals

Simply AI

Facts Made Fast

Domain-Driven Transformation

Modernize Legacy Systems and Mitigate Risk

Learning Microsoft Power Automate

Improving Productivity for Business Processes and Workflows

Practical Approach to Open Source Intelligence (OSINT)

Volume 2

Fundamentals of DevOps and Software Delivery

A Hands-On Guide to Deploying and Managing Software in Production

Technology Strategy Patterns

Analyzing and Communicating Architectural Decisions

Kubernetes - Up and Running

Dive into the Future of Infrastructure

AI Systems Performance Engineering

Optimizing Model Training and Inference Workloads with Gpus, Cuda, and Pytorch

Constraints and Advanced Solutions for LTE-Advanced Heterogeneous Networks

Building Microservices

Designing Fine-Grained Systems 2nd Edition

Digital Design and Computer Architecture

ARM Edition

This product is categorised by