Transcription
PrefaceiSystemVerilog AssertionsthHandbook, 4 editionand Formal VerificationBen CohenSrinivasan VenkataramananAjeetha Kumari.and Lisa PiperVhdlCohen PublishingLos Angeles, Californiahttp://www.SystemVerilog.us/
SystemVerilog Assertions Handbook, 4th EditioniiSystemVerilog AssertionsthHandbook, 4 Editionand Formal VerificationPublished by:VhdlCohen PublishingP.O. 2362Palos Verdes Peninsula CA 90274-2362ben@SystemVerilog.ushttp://www. SystemVerilog.us/Library of Congress Cataloging-in-Publication DataA C.I.P. Catalog record for this book is available from the Library of CongressSystemVerilog Assertions Handbook, 4th EditionDynamic and Formal VerificationISBN 978-1518681448[1] Reprinted with permission from IEEE Std. P1800/D5, 2012 -prelim Standard forSystemVerilog Unified Hardware Design,Specification, and Verification Language,Copyright 2012, by IEEE. The IEEE disclaims any responsibility or liability resulting fromthe placement and use in the described manner.Items reprinted from the above referenced IEEE document are identified with a prefix [1]and are shown in italic font.Copyright 2016 by VhdlCohen PublishingAll rights reserved. No part of this publication may be reproduced or transmitted inany form or by any means, electronic or mechanical, including photocopying,recording, or by any information storage and retrieval system, without the priorwritten permission from the author, except for the inclusion of brief quotations in areview.Printed on acid-free paperPrinted in the United States of America
PrefaceiiiContentsFOREWORD, Dennis BrophyFOREWORD, Sven BeyerFOREWORD, Stuart SutherlandPREFACEWhat's new?The creatorsHow this book addresses SVAMore about the creation of this bookHow to read this bookThe IntentBook OrganizationAcknowledgementsAbout the x.xxi.xxiii.xxviAssertions In a Verification Methodology . 11.1DESIGN VERIFICATION METHODOLOGIES . 21.2WHICH LANGUAGE/METHODOLOGY FOR PROJECT?. 31.2.1What is a property? What is an assertion? . 41.2.2Are assertions supported in frameworks? . 61.2.3Why describe same thing in RTL and assertions?. 61.3WHY SYSTEMVERILOG ASSERTIONS? . 61.3.1Are assertions independent from SystemVerilog structures?. 81.3.2Where and how are assertions used?. 81.3.2.1Capture design intent. 91.3.2.2Allow protocols to be defined and verified . 91.3.2.3Simplify usage of reusable IP . 101.3.2.4Facilitate functional coverage metrics . 101.3.2.5Generate counterexamples to demonstrate violation of properties . 10OVERVIEW OF PROPERTIES, ASSERTIONS, ATTEMPTS. 101.41.4.1Sequence. 111.4.2Cycle and range delays . 131.4.3Assertion states . 141.5ASSERTION-BASED VERIFICATION . 171.5.1Specification and verification . 171.5.2Assertions types. 181.5.2.12Concurrent assertions: assume property, assert property, cover property,cover sequence, restrict property . 18UNDERSTANDING SEQUENCES. 212.1SEQUENCE SYNTAX . 222.2SEQUENCE OPERATORS AND BUILT-IN FUNCTIONS . 232.3REPETITION OPERATORS . 262.3.1Attempt / thread difference . 272.3.1.12.3.22.3.2.1Important concepts on threads and sequences . 28Impact of multi-threaded sequences in assertions. 29Multi-threaded sequence in consequent . 31
SystemVerilog Assertions Handbook, 4th Editioniv2.3.2.1.1 Strong / weak sequence in consequent . 332.3.2.2Multi-thread sequences in both antecedent and consequent . 332.3.2.3Consequent with multiple antecedent / consequent pairs . 332.3.32.3.3.12.3.3.22.3.3.32.3.3.4Consecutive repetition . 34[*n] Repetition fixed . 34Sequence [*n:m] [*] [ ] Repetition range . 34[*0 : m] Repetition range with zero . 35[*n : ], [*] [ ] Repetition range with infinity. 362.3.4goto repetition, Boolean ([- n], [ - n:m]) . 362.3.5Non-consecutive repetition, Boolean([ n], [ n:m]) . 372.4SEQUENCE COMPOSITION OPERATORS . 382.4.1Sequence fusion (##0) and empty sequences . 392.4.2Sequence disjunction (or) . 412.4.3Sequence non-length-matching (and). 422.4.4Sequence length-matching (intersect). 422.4.5Sequence containment (within). 442.4.6Expression over sequences (throughout operator) . 452.5METHODS SUPPORTING SEQUENCES . 452.5.1first match operator . 452.5.2End point of sequences, .triggered . 472.5.3End Point of sequences, .matched .triggered . 492.5.3.12.5.4End Point of a multiclocked sequence . 50End point application examples. 512.5.4.1End points as a starting point to build sequences. 512.5.4.2Referring to the past using end points . 522.5.4.3.triggered as level-sensitive control . 532.5.4.4Sequence as events. 54ALLOWED TYPES IN FORMAL ARGUMENTS FOR SEQUENCES AND PROPERTIES . 542.62.6.12.6.22.6.32.6.42.6.4.1Formal argument of event type. 55Untyped formal argument. 56Typed formal argument: sequence. 57Data types for typed formal arguments . 58Default actual argument . 612.7LOCAL VARIABLES IN FORMAL ARGUMENTS AND IN SEQUENCE AND PROPERTY DECLARATIONS . 622.7.1Variable types, initializations, assignments, updates (rule 1, 3, 4) . 682.7.2Update of local variables (rule 15) . 692.7.3Local variables in repetitions (rule 8, 9). 702.7.4Formal arguments and local variables in sequences (rule 11, 12, 17) . 702.7.5Typed formal local variables arguments and bindings (rule 1, 13, 19) . 722.7.6No empty match in local variables assignments (rule 5). 742.7.7Local variable must be written once before being read (rule 6). 742.7.8Variable is unassigned if not flowed out (rule 7, 10) . 752.7.9Local variables in concurrent and, or, and intersect threads (rule 14). 752.7.9.12.7.9.1.12.7.9.22.7.10. 75first match(seq1 or seq2) . 77. 78.triggered method in sequences with input or inoutlocal variable formal arguments . 80
Preface3vUnderstanding Properties . 813.1ASSERTIONS, PROPERTIES, TERMINOLOGIES, SYNTAX . 813.2PROPERTY HEADER . 863.3PROPERTY IDENTIFIER . 873.4FORMAL ARGUMENTS AND USAGE . 873.4.1Formal argument representing a delay range. 893.5PROPERTY VARIABLE DECLARATION . 893.6BODY OF THE PROPERTY STATEMENT . 893.7CLOCKING EVENT . 893.7.1Leading clocking event . 903.8DISABLING CONDITION . 923.8.1Disable rules . 923.8.2Default disable. 933.8.3Inferred functions for clock and disable . 943.9PROPERTY EXPRESSION AND OPERATORS . 963.9.1Implication operators - , . 983.9.1.13.9.1.2Overlapped implication operator - . 99Non-Overlapped Implication Operator . 1003.9.2not operator. 1003.9.3and operator. 1013.9.4or operator. 1023.9.5implies. 1033.9.2.13.9.3.13.9.4.13.9.5.1Vacuity . 100Vacuity . 101Vacuity . 102Vacuity . 1033.10APPLICATIONS . 1043.10.1 iff. 1053.10.1.1Vacuity . 1063.10.2until. 1063.10.3Followed-by #-#, # # . 1083.10.4nexttime, s nexttime . 1103.10.5if else. 1113.10.6always, always[cycle delay const range], s always[bounded range] . 1113.10.7eventually, s eventually . 1143.10.8case. 1163.10.9accept on, reject on, sync accept on, reject onsync reject on . 1173.11.13.11.23.11.3Local Variable Formal Arguments . 124Using Variables as Counters . 125Using variables as Delays . 23.10.7.13.10.8.1Vacuity . 107Vacuity . 109Vacuity . 110Vacuity . 111Vacuity . 112Application example and options. 113Vacuity . 115Vacuity . 1173.10.9.1Vacuity . 1223.11 LOCAL VARIABLES IN PROPERTIES. 122
SystemVerilog Assertions Handbook, 4th Editionvi3.11.44Using Variables as Timeouts. 127Advanced Topics For Properties and Sequences. 1314.1SYSTEMVERILOG SCHEDULING SEMANTICS FOR ASSERTIONS. 1314.2ASSERTION-BASED SYSTEM FUNCTIONS . 1344.2.1Sampled valued functions. 1344.2.1.1Value access functions . 1344.2.1.1.1 sampled(expression) . 1344.2.1.1.1.1 sampled in a disable iff clause . 1344.2.1.1.1.2 sampled in an action block. 1354.2.1.1.2 past. 1364.2.1.2Value change functions . 1374.2.1.2.1 rose and fell . 1374.2.1.2.2 stable, changed . 1384.2.24.2.3Vector-analysis system functions . 139Severity-level system functions. 1404.2.4Assertion-control system tasks . 1434.2.3.14.2.3.2SystemVerilog severity levels . 140UVM severity levels . 1424.2.4.1Assert control. 1444.2.4.1.1 Control type . 1454.2.4.1.2 assertion type. 1484.2.4.1.3 directive type . 1484.2.4.1.4 Equivalent assertion control system tasks . 1484.2.4.1.5 Assertion action blocks -control system tasks. 149CLOCKED SEQUENCES, PROPERTIES, AND MULTICLOCKING . 1504.34.3.1Multiclocked Sequences and Properties . 1514.3.2Clocking Rules in Assertions. 1534.3.3Clock Flow . 1534.3.4Procedural Concurrent Assertion. 1554.3.5Arguments to Procedural Concurrent Assertions . 1584.4PROPERTIES IN INTERFACES . 1604.5ASSERTION STATEMENTS . 1614.5.1Purpose of verification statements. 1634.5.1.1assert Statement . 1634.5.1.2assume statement. 1644.5.1.2.1 assert and assume for same property: then what?. 1654.5.1.2.2 Same inputs in antecedent and consequent . 1654.5.1.3restrict statement . 1654.5.1.4cover statement . 1664.5.1.4.1 Understanding coverage . 1674.5.1.4.2 Using covergroup for data coverage . 1694.5.1.5Expect construct. 1704.5.1.6Action-Block . 1724.5.2Assertions in RTL. 1724.6IMMEDIATE ASSERTIONS . 1734.6.1Simple immediate assertions. 1744.6.2Deferred assertions. 1754.6.2.1Deferred assertion reporting . 1774.7BINDING ASSERTIONS TO SCOPES OR INSTANCES . 1784.8STATIC / AUTOMATIC VARIABLES AND ASSERTIONS . 1824.8.1Static / automatic variable defintions . 1824.8.2Sampling of variables in assertions . 183
Preface5viiCHECKER . 1875.1MOTIVATION AND ADVANTAGES OF CHECKER CONSTRUCT . 1875.2SYNTAX OF CHECKER CONSTRUCT. 1895.3CHECKER CONTENTS. 1905.4CHECKER USE MODEL . 1925.4.1Classification of assertion statements. 1925.4.2Classification of checker Instances . 1935.4.3Checker behaviors based on types and instances. 1935.4.3.1checker usages . 1985.4.3.1.1 Self-sustained independent checker declaration with direct of bind instantiation . 1985.4.3.1.2 Checker declared and instantiated inside design unit (module, interface,checker, or program) . 1995.4.3.1.3 Checker declared in packages that are instantiated inside the design unit . 2005.4.3.1.4 checker bound to a design unit . 201CONTEXT INFERENCE . 202CHECKER VARIABLES . 2035.55.65.6.15.6.25.6.36Static and automatic variables. 203rand and rand const variables . 204Capturing functional coverage model inside checker. 205SystemVerilog Assertions In the Design Process. 2076.1TRADITIONAL DESIGN PROCESS . 2086.2DESIGN PROCESS WITH SVA . 2086.2.1System-level Assertions . 2086.3REQUIREMENTS . 2096.3.1Cause and effect class of requirements . 2096.3.2Latencies . 2096.3.3Definition of Processing Algorithms . 2106.3.4Interface Assertions . 2116.4ARCHITECTURAL PLAN . 2116.5VERIFICATION AND TEST PLAN . 2126.6RTL DESIGN . 2136.7TESTBENCH DESIGN . 2136.8FUNCTIONAL COVERAGE IN VERIFICATION . 2136.8.1SystemVerilog Assertions API . 2146.8.2Formal verification (FV) . 2176.9CASE STUDY - SYNCHRONOUS FIFO. 2176.9.1Synchronous FIFO Requirements . 2176.9.2Test Plan . 2286.10 RTL DESIGN . 2356.11 SIMULATION . 235
SystemVerilog Assertions Handbook, 4th Editionviii7FORMAL VERIFICATION USING Assertions . 2377.1FORMAL PROPERTY VERIFICATION .
Preface i SystemVerilog Assertions Handbook, 4th edition and Formal Verification Ben Cohen Srinivasan Venkataram
