第1页 / 共589页
第2页 / 共589页
第3页 / 共589页
第4页 / 共589页
第5页 / 共589页
第6页 / 共589页
第7页 / 共589页
第8页 / 共589页
SVA_ The Power of Assertions in SystemVerilog.pdf
Preface
Acknowledgments
Contents
Acronyms
Part I Opening
1 Introduction
1.1 The Concept of Assertion
Implementing Checks in Verilog Is Difficult
Assertions Formally Express Design Intent
Assertions Improve Bug Detection
Assertions Promote Faster Root Cause Analysis
Assertions Can Use Simulation and Formal Checking
Assertions Are Part of Design Documentation
1.2 Assertions in Design Methodology
1.2.1 Using Assertions for High Level Model
1.2.2 Using Assertions for RTL Models
Assertions on Interfaces
Embedding Assertions Within Design
Assertion Coverage
Coverage-Based Verification
1.2.3 Using Assertions Beyond RTL
Equivalence Verification
Timing Verification
Post-Silicon Validation
1.3 Assertions in SystemVerilog
Assertion Statements
1.4 Checking Assertions
1.4.1 Checking Assertions in Simulation
1.4.2 Checking Assertions Using Hardware Acceleration
1.4.3 Checking Assertions Using Formal Verification
1.4.4 Assertion Efficiency
1.5 Assertion Reuse
Expression Reuse
Sequence Reuse
Property Reuse
Assertion Libraries
1.6 SVA and PSL
Exercises
2 SystemVerilog Language Overview
2.1 Compilation and Elaboration
2.2 SystemVerilog Procedures
2.2.1 Specialized Always Procedures
2.2.1.1 Procedure always_comb
2.2.1.2 Procedure always_latch
2.2.1.3 Procedure always_ff
2.2.2 Final Procedure
2.3 Clocking Blocks
2.3.1 Clocking Block Declaration
2.3.2 Default Clocking
2.4 Interfaces
2.5 Programs
2.6 Packages
Exercises
3 SystemVerilog Simulation Semantics
3.1 Event Based Simulation
3.2 The Simulation Engine
3.3 Bringing Order to Events
3.4 Determinism and Nondeterminism
3.5 Region Sets
3.6 A Time Slot and the Movement of Time
3.7 Simulation Semantics of Assignments
Exercises
Part II Basic Assertions
4 Assertion Statements
4.1 Assertion Kinds
4.2 Immediate Assertions
4.2.1 Immediate Assertion Simulation
4.2.2 Simulation Glitches
4.2.3 Effect of Short-Circuiting
4.3 Deferred Assertions
4.3.1 Deferred Assertion Simulation
4.3.2 Deferred Assertion Actions
4.3.3 Standalone Deferred Assertions
4.3.4 Effect of Short-Circuiting in Deferred Assertions
4.4 Concurrent Assertions
4.4.1 Simulation Evaluation Attempt
4.4.2 Clock
Gated Clock
Global Clocking
4.4.3 Sampled Values for Concurrent Assertion
4.4.4 Reset
4.4.5 Boolean Expressions
4.4.6 Event Semantics for Concurrent Assertions
4.5 Assumptions
4.5.1 Motivation
4.5.2 Assumption Definition
4.5.3 Checking Assumptions
4.5.3.1 Assumptions in Simulation and Emulation
4.5.3.2 Assumptions in Formal Verification
4.5.3.3 Assumptions in Random Simulation
4.6 Restrictions
4.7 Coverage
4.7.1 Motivation
4.7.2 Coverage Definition
4.7.2.1 Concurrent Coverage
4.7.3 Checking Coverage
4.7.3.1 Checking Coverage in Simulation
4.7.3.2 Checking Coverage in Formal Verification
4.8 Summary of Checking Assertions
Exercises
5 Basic Properties
5.1 Boolean Property
5.2 Nexttime Property
5.3 Always Property
5.3.1 Implicit Always Operator
5.4 S_eventually Property
5.5 Basic Boolean Property Connectives
5.6 Until Property
Exercises
6 Basic Sequences
6.1 Boolean Sequence
6.2 Sequential Property
6.3 Sequence Concatenation
6.3.1 Multiple Delays
6.3.2 Top-Level Sequential Properties
6.3.3 Sequence Fusion
6.3.4 Initial Delay
6.4 Suffix Implication
6.4.1 Nested Implication
6.4.2 Examples
6.4.3 Vacuous Execution
6.5 Consecutive Repetition
6.5.1 Zero Repetition
6.5.1.1 Concatenation with Empty Sequence
6.5.1.2 Fusion with Empty Sequence
6.5.1.3 Empty Sequence in Antecedent
6.6 Sequence Disjunction
6.7 Consecutive Repetition Revisited
6.7.1 Repetition Range
6.7.1.1 Finite Repetition Range
6.7.1.2 Infinite Repetition Range
6.8 Sequences Admitting Empty Match
6.8.1 Antecedents Admitting Empty Match
6.9 Sequence Concatenation and Delay Revisited
6.10 Unbounded Sequences
Exercises
7 Assertion System Functions and Tasks
7.1 Bit Vector Functions
7.1.1 Count Bits with Specific Values
7.1.2 Check for Mutual Exclusion
7.1.3 One-Hot Encoding
7.1.4 Number of 1-Bits
7.1.5 Unknown Bits
7.2 Sampled Value Functions
7.2.1 General Sampled Value Functions
7.2.1.1 Present Sampled Values
7.2.1.2 Past Sampled Values
7.2.1.3 Rose and Fell
7.2.1.4 Changed and Stable
7.2.1.5 Clock Inference
7.2.2 Global Clocking Sampled Value Functions
7.2.2.1 Past Global Clocking Sampled Value Functions
7.2.2.2 Future Global Clocking Sampled Value Functions
7.3 Tasks for Controlling Assertions and Runtime Violations
7.3.1 Tasks for Controlling Evaluation Attempts
7.3.2 Tasks for Controlling Action Blocks
7.3.3 General Assertion Control Task
Exercises
Part III Metalanguage Constructs
8 Let, Sequence and Property Declarations; Inference
8.1 Let Declarations
8.1.1 Syntax of Let
8.1.2 Uses of Let
8.2 Sequence and Property Declarations
8.2.1 Syntax of Sequence–Endsequence
8.2.2 Syntax of Property–Endproperty
8.3 Disable Expression and Clock Inference
Exercises
9 Checkers
9.1 An Apology for Checkers: Sequential Protocol
9.1.1 Sequential Protocol Specification as Module
9.1.2 Sequential Protocol as Checker
9.2 Checker Declaration
9.2.1 Checker Formal Arguments
9.2.1.1 Argument Direction
9.2.1.2 Default Arguments
9.2.1.3 Context Inference
9.2.1.4 Checker Argument Types
9.2.2 Checker Contents
9.2.2.1 Generate Constructs
9.2.2.2 Checker Procedures
9.2.3 Scoping Rules
9.2.3.1 Checkers in Packages
9.3 Checker Instantiation
9.3.1 Connecting Checker Arguments
9.3.1.1 Positional Association
9.3.1.2 Explicit Named Association
9.3.1.3 Implicit Named Association
9.3.1.4 Wildcard Named Association
9.3.2 Instantiation Semantics
9.3.2.1 Object Naming
9.3.2.2 Context Inference and Name Resolution
9.3.3 Checker Binding
9.4 Checker Modeling
9.4.1 Checker Variables
9.4.1.1 Functions in Checkers
9.4.2 Sampling in Checkers
9.4.3 Checker Variables in Final Procedures
9.5 Checkers with Output Arguments
9.5.1 Checker Output Arguments
9.5.1.1 Checker Output Argument Typing
9.5.1.2 Checker Output Argument Initialization
9.5.1.3 Semantics of Checker Output Arguments
9.5.2 Returning Assertion Status from Checkers
9.5.3 Writing Modular Checkers
Exercises
Part IV Advanced Assertions
10 Advanced Properties
10.1 Sequential Property
10.2 Boolean Property Operators
Negation
Disjunction
Conjunction
Implication
Equivalence
If [Else]
Case
10.3 Suffix Operators: Implication and Followed-By
Suffix Implication
Suffix Conjunction (Followed-By)
10.4 Unbounded Linear Temporal Operators
Until
Always and S_eventually
Until_with
10.5 Bounded Linear Temporal Operators
Nexttime
Bounded Eventually and Always Operators
10.6 Vacuous Evaluation
Exercises
11 Advanced Sequences
11.1 Sequence Operators
11.1.1 Throughout
11.1.2 Goto Repetition
11.1.3 Nonconsecutive Repetition
11.1.4 Intersection
11.1.5 Sequence Conjunction
11.1.6 Sequence Containment
11.1.7 First Match of a Sequence
11.2 Sequence Methods
11.2.1 Triggered: Detecting End Point of a Sequence
11.2.1.1 Past Temporal Operators
11.2.1.2 Triggered Outside Assertions in RTL
11.2.2 The triggered Method in Checkers
11.2.3 Matched
11.3 Sequence as Events
11.3.1 Sequence Event Control
11.3.2 Level-Sensitive Sequence Control
11.3.3 Event Semantics of Sequence Match
Exercises
12 Clocks
12.1 Overview of Clocks
12.1.1 Specifying Clocks
12.1.2 Multiple Clocks
12.2 Further Details of Clocks
12.2.1 Preponed Value Sampling
12.2.2 Default Clocking
12.2.3 Restrictions in Multiply Clocked Sequences
12.2.4 Scoping of Clocks
12.2.4.1 Clock Flow
12.2.4.2 Semantic Leading Clocks
12.2.5 Finer Points of Multiple Clocks
12.2.5.1 Clocking LTL Operators
12.2.5.2 Unclocked Synchronizers and Logical Operators
12.2.5.3 Continuity Under Clock Convergence
12.2.5.4 Sequence Methods
12.2.6 Declarations Within a Clocking Block
Exercises
13 Resets
13.1 Overview of Resets
13.1.1 Disable Clause
13.1.1.1 Default Disable Condition
13.1.2 Aborts
13.1.2.1 Asynchronous Aborts
13.1.2.2 Synchronous Aborts
13.2 Further Details of Resets
13.2.1 Generalities of Reset Conditions
13.2.2 Aborts as Subproperties
Exercises
14 Procedural Concurrent Assertions
14.1 Using Procedural Context
14.2 Clock Inferencing
14.3 Using Automatic Variables
14.4 Assertions in a For-Loop
14.5 Event Semantics of Procedural Concurrent Assertions
14.6 Things to Watch Out For
14.7 Dealing with Unwanted Procedural Assertion Evaluations
14.8 Procedural Checker Instances
Exercises
15 An Apology for Local Variables
15.1 Fixed Latency Data Pipeline
15.2 Sequential Protocol
15.3 FIFO Protocol
15.4 Tag Protocol
15.5 FIFO Protocol Revisited
15.6 Tag Protocol Revisited
15.6.1 Tag Protocol Using a Single Static Bit
15.6.2 Tag Protocol Using Only Local Variables
Exercises
16 Mechanics of Local Variables
16.1 Declaring Body Local Variables
16.2 Declaring Argument Local Variables
16.3 Assigning to Local Variables
16.3.1 Assignment Within Repetition
16.3.2 Sequence Match Items
16.4 Referencing Local Variables
16.4.1 Local Variable Flow
16.4.2 Becoming Unassigned
16.4.3 Multiplicity of Matching with Local Variables
16.5 Input and Output with Local Variables
16.5.1 Input with Local Variables
Exception for Sequence Methods
16.5.2 Output with Local Variables
Exercises
17 Recursive Properties
17.1 Overview of Recursion
17.2 Retry Protocol
17.3 Restrictions on Recursive Properties
17.3.1 Negation and Strong Operators
17.3.2 Disable Clause
17.3.3 Time Advance
17.3.4 Actual Arguments
Exercises
18 Coverage
18.1 Immediate and Deferred Coverage
18.2 Sequence and Property Coverage
18.2.1 Sequence Coverage
18.2.2 Property Coverage
18.2.3 Covergroup
18.2.4 Combining Covergroups and Assertions
18.3 Covergroups in Checkers
18.4 Coverage on Weak and Strong Properties
18.5 Examples
Exercises
19 Debugging Assertions and Efficiency Considerations
19.1 Debugging an Assertion Under Development
19.2 Debugging Assertion Failures from a Test
19.3 Efficiency Considerations
Compile Time Performance
Run Time Performance
Exercises
Part V Formal Verification
20 Introduction to Assertion-Based Formal Verification
20.1 Counterexample and Witness
20.2 Complete and Incomplete Methods
20.3 Approximation
20.3.1 Overapproximation
20.3.2 Underapproximation
Empty Model
20.3.3 Pruning
20.4 Formal Verification Flows
20.4.1 Exhaustive Verification of Model Specification
20.4.2 Lightweight Verification
20.4.3 Early RTL Verification
20.5 Assume-Guarantee Paradigm
20.6 Formal Verification Efficiency
20.7 Hybrid Verification
Exercises
21 Formal Verification and Models
21.1 Auxiliary Notions
21.1.1 Relations
21.1.2 Logic Notation and Quantifiers
21.1.3 Languages
21.1.4 Finite Automaton
21.2 Formal Verification Model
21.2.1 Time
21.2.2 Model Language
21.2.3 Symbolic Representation
21.2.3.1 Sampled Value Functions
21.3 Properties
21.3.1 Asserts
21.3.2 Assumes
21.3.3 Coverage
21.3.4 Constraining a Model with Assumptions
21.4 Safety and Liveness
21.4.1 Safety Properties
21.4.2 Liveness Properties
21.4.2.1 Why Write Liveness Properties?
21.4.2.2 Counterexamples for Liveness Properties
21.4.2.3 Assumptions and Liveness
21.4.2.4 Automata of Clocked Properties
21.5 Weak and Strong Operators
Suffix Implication
Negation
Operator Composition
21.6 Embedded Assertions
21.7 Immediate and Deferred Assertions
Exercises
22 Formal Semantics
22.1 Formal Semantics of Properties
22.1.1 Basic Property Forms
22.1.1.1 Boolean Property
22.1.1.2 Negation Property
22.1.1.3 Conjunction Property
22.1.1.4 Nexttime Property
22.1.1.5 Strong Until Property
22.1.2 Derived Properties
22.1.2.1 Boolean Connectives
22.1.2.2 Eventually Property
22.1.2.3 Always Property
22.1.2.4 Until Properties
22.2 Formal Semantics of Sequences
22.3 Formal Semantics: Sequences and Properties
22.3.1 Strong Sequential Property
22.3.2 Extension of Alphabet
22.3.3 Weak Sequential Property
22.3.4 Property Negation
22.3.5 Suffix Implication
22.3.6 Suffix Conjunction: Followed-by
22.4 Formal Semantics of Clocks
22.5 Formal Semantics of Resets
22.6 Formal Semantics of Local Variables
22.6.1 Formalizing Local Variable Flow
22.6.2 Local Variable Contexts
22.6.3 Sequence Semantics with Local Variables
22.6.4 Property Semantics with Local Variables
22.7 Formal Semantics of Recursive Properties
Exercises
Part VI Advanced Checkers
23 Checkers in Formal Verification
23.1 Free Variables
23.1.1 Free Variables in Assertions
23.1.2 Free Variables in Assumptions
23.1.3 Free Variables in Cover Statements
23.2 Checker Modeling with Free Variables
23.2.1 Free Variable Initialization
23.2.2 Free Variable Assignment
23.2.2.1 Unconditional Assignment to Free Variables
23.2.2.2 Conditional Assignment to Free Variable
23.2.2.3 Fully Assigned Free Variables
23.2.2.4 Assigning Free Variables to Checker Variables
23.2.2.5 Checker Data Model
23.2.3 Example: Building Abstract Models with Checkers
23.3 Free Variables in Simulation
23.3.1 Unconstrained Free Variables
23.3.2 Assigned Free Variables
23.3.3 Checkers with Assumptions
23.3.4 Limitations Imposed on Free Variables
23.4 Rigid Variables
23.4.1 Rigid Variables in Formal Verification
23.4.2 Rigid Variable Support in Simulation
23.4.3 Rigid and Free Variables Versus Local Variables
23.5 Checkers as Generators
Exercises
24 Checker Libraries
24.1 Weaknesses of Existing Checker Libraries
24.2 Kinds of Checkers and Their Characteristics
24.2.1 Temporality
24.2.2 Encapsulation
24.2.3 Packaging
24.2.4 Configurability
24.3 Examples of Typical Checker Kinds
24.3.1 Simple Combinational Checker
24.3.2 A Checker-Based Combinational Checker
24.3.3 A Simple Property-Based Temporal Checker
24.3.4 A Checker-Based Temporal Checker
24.4 Converting Module-Based Checkers to the New Format
Exercises
Appendix
A Expression Sampling
A.1 Default Sampled Value
A.2 Sampled Value of Variable
A.3 Sampled Value of Expression
References
Index
Eduard Cerny · Surrendra Dudani
John Havlicek · Dmitry Korchemny
SVA: The Power
of Assertions in
SystemVerilog
Second Edition
SVA: The Power of Assertions in SystemVerilog
Eduard Cerny • Surrendra Dudani John Havlicek
Dmitry Korchemny
SVA: The Power of
Assertions in SystemVerilog
Second Edition
123
Eduard Cerny
Synopsys, Inc.
Worcester
MA, USA
John Havlicek
Cadence Design Systems
Austin, TX, USA
Surrendra Dudani
Synopsys, Inc.
Newton, MA, USA
Dmitry Korchemny
Intel, Kfar Saba, Israel
ISBN 978-3-319-07138-1
DOI 10.1007/978-3-319-07139-8
Springer Cham Heidelberg New York Dordrecht London
ISBN 978-3-319-07139-8 (eBook)
Library of Congress Control Number: 2014942642
© Springer International Publishing Switzerland 2010, 2015
This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part of
the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations, recitation,
broadcasting, reproduction on microfilms or in any other physical way, and transmission or information
storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar methodology
now known or hereafter developed. Exempted from this legal reservation are brief excerpts in connection
with reviews or scholarly analysis or material supplied specifically for the purpose of being entered
and executed on a computer system, for exclusive use by the purchaser of the work. Duplication of
this publication or parts thereof is permitted only under the provisions of the Copyright Law of the
Publisher’s location, in its current version, and permission for use must always be obtained from Springer.
Permissions for use may be obtained through RightsLink at the Copyright Clearance Center. Violations
are liable to prosecution under the respective Copyright Law.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication
does not imply, even in the absence of a specific statement, that such names are exempt from the relevant
protective laws and regulations and therefore free for general use.
While the advice and information in this book are believed to be true and accurate at the date of
publication, neither the authors nor the editors nor the publisher can accept any legal responsibility for
any errors or omissions that may be made. The publisher makes no warranty, express or implied, with
respect to the material contained herein.
Printed on acid-free paper
Springer is part of Springer Science+Business Media (www.springer.com)
Preface
This book is the result of the deep involvement of the authors in the development of
EDA tools, SystemVerilog Assertion standardization, and many years of practical
experience. One of the goals of this book is to expose the oral knowhow circulated
among design and verification engineers which has never been written down in
its full extent. The book thus contains many practical examples and exercises
illustrating the various concepts and semantics of the SystemVerilog assertion
language. Much attention is given to discussing efficiency of assertion forms in
simulation and formal verification. We did our best to validate all the examples, but
there are hundreds of them and not all features could be validated since they have
not yet been implemented in EDA tools. Therefore, we will be grateful to readers for
pointing to us any needed corrections. The book is written in a way that we believe
serves well both the users of SystemVerilog assertions in simulation and also those
who practice formal verification (model checking). Compared to previous books
covering SystemVerilog assertions we include in detail the most recent features
that appeared in the IEEE 1800–2009 SystemVerilog Standard and were further
improved and enhanced in the recent IEEE 1800–2012 Standard. In particular, it
concerns the new encapsulation construct “checker” and checker libraries, Linear
Temporal Logic operators, and semantics and usage in formal verification. However,
for integral understanding we present the assertion language and its applications in
full detail.
This second edition of the book not only introduces the enhancements and
corrections present in the 2012 SystemVerilog standard, but also it is reorganized
in a way that facilitates basic assertion understanding, initial deployment in simple
forms, fully detailed exposition of the power of the language, and deployment in
simulation and formal verification. Not to mention corrections to several errors and
inconsistencies in the first edition.
The book is divided into six parts. These parts are organized from introductory
to advanced, as well as separating as much as possible aspects related to simulation
and formal verification. Part I is enough to get basic understanding of SystemVerilog
v
vi
Preface
Assertions. By adding Part II, the reader should be able to write typical assertions
and use them in simulation. Parts III and IV provide deep understanding of the
assertion language. Part V is dedicated to formal verification and provides formal
semantics of the language. Finally, Part VI deals with the design of checker libraries
and the use of checkers in formal verification. The Appendix concisely describes
sampling of variables, as it is different than in the previous 2009 Standard and thus
the 1st edition of this book.
Part I, Opening, is an extended introduction to assertions, their use in simula-
tion, formal verification and other tools, and their meaning in relation to the rest of
the SystemVerilog language.
Chapter 1 introduces the concept of assertions, their place in history of design
verification, and discusses the use of assertions in hardware design and verification
flow.
Chapter 2 introduces minimal necessary concepts from the SystemVerilog
language, other than assertions, that are useful for understanding assertions and their
usage.
Chapter 3 provides the basics of SystemVerilog simulation semantics. It dis-
cusses how SystemVerilog processes are executed in the various scheduling regions
and how assertions interact with the simulation of the design model.
Part II, Basic Assertions, goes into sufficient details of the assertion language
to understand and write simple assertions.
Chapter 4 describes the different assertion statements that can be used to ascertain
correctness, provide constraints and collect coverage, both in clocked concurrent
and unclocked immediate (simple and deferred) forms.
Chapters 5 and 6 provide the basic information on how to write simple properties
and sequences that form the operational core of assertions.
Chapter 7 exposes system functions that help to write assertions without having
to resort to additional procedural code and introduces several system tasks for
controlling assertion and action block execution. The main difference with the
earlier version of the standard is the introduction of a more powerful function to
detect the presence of x and z signal values and a unified task for controlling the
execution of assertions.
Part III Metalanguage Constructs
Chapter 8 considers reusability of assertion bodies by showing how Boolean
expressions, sequences, and properties can be defined and parameterized for later
reuse.
Chapter 9 provides a detailed exposition of the encapsulation construct “checker.”
This construct is the basis for forming what could be called a super assertion, that
is, an assertion entity that combines procedural code, modeling variables, variable
assignments, coverage, assertion and assumption statements into one reusable
parameterized unit. Checkers now allow different kinds of procedures as well as
continuous assignments which were illegal previously. Sampling as described in the
Appendix has also changed in checkers.
Preface
vii
Part IV Advanced Assertions
Chapters 10 and 11 delve into the full intricacies of property and sequence
operators. The former chapter also defines precisely the notions of vacuous and
non-vacuous evaluations of assertions.
Chapter 12 describes sampling clocks, clock flow through assertions, and
multiclocked assertions.
Chapter 13 provides information on the ways synchronous property evaluation
can be terminated with success or failure using asynchronous and synchronous abort
operators.
Chapter 14 shows how to use concurrent assertions inside always procedures,
and how the leading clock is inferred. It also describes how evaluation attempts are
started depending on the conditional and looping statements inside procedures.
Chapter 15 apologizes for local variables, but in fact shows how local variables
provide much flexibility to assertions, especially in simulation.
Chapter 16 exposes the various forms of local variable declarations and rules of
deployment, including special local variable arguments to properties and sequences.
Chapter 17 shows another facet of SystemVerilog assertions, that of recursive
properties. They provide an alternate and succinct form for expressing complex
properties.
Chapter 18 discusses coverage collection that is needed to measure the verifi-
cation progress. Two forms are described, using assertion cover statements alone
and in combination with test bench covergroups to form powerful data collection
constructs.
Chapter 19 briefly introduces some techniques for debugging assertions, inde-
pendently of services provided by specific EDA tools, and then discusses the
efficiency of various assertion forms in simulation and formal verification.
Part V Formal Verification
Chapter 20 provides an introduction to the treatment of assertions in formal
verification by discussing the different ways formal verification can proceed and
its role in the verification process.
Chapter 21 exposes details of the models and algorithms used in formal
verification, in particular, model checking.
Chapter 22 gives the theoretical base for full and precise understanding of
the meaning of assertions. This chapter is particularly important to anyone who
implements some form of an assertion verification engine, simulation or formal.
Part VI, Advanced Checkers, is primarily concerned with developing effective
reusable verification objects.
Chapter 23 shows how checkers can be used effectively in formal verification.
The chapter also provides deeper understanding of the behavior of checker variables.
Chapter 24 discusses how to create libraries of verification statements based on
assertions, from simple let or property based forms, to the complex ones using
checker encapsulation.
We did our best to verify and compile each and every example and verify the
text, however, not all SystemVerilog constructs introduced in the 2009 and 2012
standards are supported by commercial tools. In spite of the great improvements in
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
