SVA : The Power of Assertions in SystemVerilog

By: Cerny, EduardContributor(s): Dudani, Surrendra | Havlicek, John | Korchemny, DmitryMaterial type: TextTextSeries: eBooks on DemandPublisher: Dordrecht : Springer, 2014Edition: 2nd edDescription: 1 online resource (589 p.)ISBN: 9783319071398Subject(s): Integrated circuits -- Verification -- Data processing | Quantum computers | Verilog (Computer hardware description language)Genre/Form: Electronic books.Additional physical formats: Print version:: SVA : The Power of Assertions in SystemVerilogDDC classification: 004.1 | 621.381548 LOC classification: TK7874.58Online resources: Click here to view this ebook.
Contents:
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 Verification1.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 Procedures2.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 Assertions4 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 Assertions4.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
Summary: This book is a comprehensive guide to assertion-based verification of hardware designs using System Verilog Assertions (SVA). It enables readers to minimize the cost of verification by using assertion-based techniques in simulation testing, coverage collection and formal analysis. The book provides detailed descriptions of all the language features of SVA, accompanied by step-by-step examples of how to employ them to construct powerful and reusable sets of properties.?The book also shows how SVA fits into the broader System Verilog language, demonstrating the ways that assertions can interact
Tags from this library: No tags from this library for this title. Log in to add tags.
Item type Current location Call number URL Status Date due Barcode
Electronic Book UT Tyler Online
Online
TK7874.58 (Browse shelf) http://uttyler.eblib.com/patron/FullRecord.aspx?p=1802619 Available EBL1802619

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 Verification1.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 Procedures2.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 Assertions4 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 Assertions4.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

This book is a comprehensive guide to assertion-based verification of hardware designs using System Verilog Assertions (SVA). It enables readers to minimize the cost of verification by using assertion-based techniques in simulation testing, coverage collection and formal analysis. The book provides detailed descriptions of all the language features of SVA, accompanied by step-by-step examples of how to employ them to construct powerful and reusable sets of properties.?The book also shows how SVA fits into the broader System Verilog language, demonstrating the ways that assertions can interact

Description based upon print version of record.

Author notes provided by Syndetics

Eduard Cerny received M.Eng. and Ph.D. degrees in electrical engineering from McGill University, Montreal, in 1970 and 1975, respectively. From 1978 until 2001 he was a professor in the Department Computer Science and Operations Research at the Universite de Montreal. He published and was a consultant in areas related to the specification, simulation, formal verification and test of microelectronics systems and in the development of CAD tools. He joined Synopsys, Inc., in 2001. Currently he is a Scientist in the Marlborough, MA, office as member of the Synopsys Verification Group. His responsibilities include design-for-verification methodology, in particular as related to assertions, with four patents in that area. He was co-chair and member of the IEEE P1800 System Verilog Assertions committee and a co-author of the books Verification Methodology Manual for System Verilog (Kluwer 2006) and The Power of System Verilog Assertions (Springer 2010).

Surrendra Dudani received M.S. and Ph.D. degrees in electrical & computer engineering from Syracuse University, NY, in 1976 and 1980, respectively. From 1980 until 1989, he worked at Honeywell, Prime Computers and Stardent Computers as a Principal Engineer. He developed various design verification languages, CAD tools and methodologies. In 1990, he founded Pragmatics Computing to provide consulting services to hardware and software companies. He pioneered code coverage technology for design verification and introduced one of the first products in the market. He joined Synopsys, Inc., in 1999. Currently he is a Scientist in the Marlborough, MA, office as member of the Synopsys Verification Group. His current responsibilities include developing and managing assertions technology and other techniques for design verification. He holds three patents and has published many papers at conferences. He was a member of the IEEE P1800 System Verilog Assertions committee and a co-author of The Power of System Verilog Assertions (Springer 2010).

John Havlicek earned a B.S. in Mathematics from Ohio State (1987) and a Ph.D. in Mathematics from Stanford (1992). From 1996 to 2000, he pursued doctoral studies in Computer Sciences at the University of Texas, working on formal methods with E. Allen Emerson. He then joined Motorola Semiconductor and began work on tools and methodologies for semiconductor design verification. He has worked to expand the deployment of assertions both in simulation and formal verification and has been active in the creation and standardization of industrial assertion languages, notably IEEE 1850 PSL and IEEE 1800 System Verilog Assertions. He served as chair of the System Verilog Assertions Committee, served on the System Verilog Champions Committee and helped to found the System Verilog Discrete Committee. He was a primary author of enhancements to coverage modeling capabilities in the 2012 System Verilog standard. He also worked in a subgroup of the Verilog-AMS Committee to study assertion constructs for analog and mixed-signal verification. Currently, he works for Cadence Design Systems in the Design IP Team for DDR Memory Controller and PHY. As diversions, John enjoys early music, backpacking and amateur astronomy.

Dmitry Korchemny earned an MSc. in electrical engineering and computer science from Moscow Institute of Radio-engineering, Electronics and Automation in 1984. He joined Intel in 1993. Currently he is a senior CAD technical staff engineer at Intel. His interests include pre- and post-Si verification, debug and test generation. He is actively involved into System Verilog Assertion standardization and he is a chair of Assertion Committee of IEEE P1800 Working Group.

There are no comments on this title.

to post a comment.