Assertion-Based Design
Autor Harry D. Foster, Adam C. Krolnik, David J. Laceyen Limba Engleză Paperback – 14 oct 2012
Preț: 381.80 lei
Puncte Express: 573
Carte tipărită la comandă
Livrare economică 08-22 iulie
Livrare prin curier în România Termenul estimat este afișat lângă disponibilitate.
Transport gratuit de la 400.00 lei Plată online sau ramburs, în funcție de opțiunile comenzii.
Retur gratuit în 14 zile Comandă securizată și suport în română.
Specificații
ISBN-13: 9781461348481
ISBN-10: 146134848X
Pagini: 388
Ilustrații: XXII, 363 p.
Dimensiuni: 155 x 235 x 21 mm
Greutate: 0.59 kg
Ediția:Softcover reprint of the original 1st ed. 2003
Editura: Springer
Locul publicării:New York, NY, United States
ISBN-10: 146134848X
Pagini: 388
Ilustrații: XXII, 363 p.
Dimensiuni: 155 x 235 x 21 mm
Greutate: 0.59 kg
Ediția:Softcover reprint of the original 1st ed. 2003
Editura: Springer
Locul publicării:New York, NY, United States
Public țintă
ResearchCuprins
1 Introduction.- 1.1 Property checking.- 1.2 Verification techniques.- 1.3 What is an assertion?.- 1.4 Phases of the design process.- 1.5 Summary.- 2 Assertion Methodology.- 2.1 Design methodology.- 2.2 Assertion methodology for new designs.- 2.3 Assertion methodology for existing designs.- 2.4 Assertions and simulation.- 2.5 Assertions and formal verification.- 2.6 Summary.- 3 Specifying RTL Properties.- 3.1 Definitions and concepts.- 3.2 Property classification.- 3.3 RTL assertion specification techniques.- 3.4 Pragma-based assertions.- 3.5 SystemVerilog assertions.- 3.6 PCI property specification example.- 3.7 Summary.- 4 PLI-Based Assertions.- 4.1 Procedural assertions.- 4.2 PLI-based assertion library.- 4.3 Summary.- 5 Functional Coverage.- 5.1 Verification approaches.- 5.2 Understanding coverage.- 5.3 Does functional coverage really work?.- 5.4 Functional coverage methodology.- 5.5 Specifying functional coverage.- 5.6 Functional coverage examples.- 5.7 AHB example.- 5.8 Summary.- 6 Assertion Patterns.- 6.1 Introduction to patterns.- 6.2 Signal patterns.- 6.3 Set patterns.- 6.4 Conditional patterns.- 6.5 Past and future event patterns.- 6.6 Window patterns.- 6.7 Sequence patterns.- 6.8 Applying patterns to a real example.- 6.9 Summary.- 7 Assertion Cookbook.- 7.1 Queue—FIFO.- 7.2 Fixed depth pipeline register.- 7.3 Stack—LIFO.- 7.4 Caches—direct mapped.- 7.5 Cache—set associative.- 7.6 FSM.- 7.7 Counters.- 7.8 Multiplexers.- 7.9 Encoder.- Appendix A Open Verification Library.- A.1 OVL methodology advantages.- A.2 OVL standard definition.- A.2.1 OVL runtime macro controls.- A.2.2 Customizing OVL messages.- A.3 Firing OVL monitors.- A.4 Using OVL assertion monitors.- A.5 Checking invariant properties.- A.5.1 assert_always.- A.5.2 assert_never.- A.5.3 assert_zero_ one_ hot.- A.5.4 assert_range.- A.6 Checking cycle relationships.- A.6.1 assert_next.- A.6.2 assert_frame.- A.6.3 assert_cycle_sequence.- A.7 Checking event bounded windows.- A.7.1 assert_win_change.- A.7.2 assert_win_unchange.- A.8 Checking time bounded windows.- A.8.1 assert_change.- A.8.2 assert_unchange.- A.9 Checking state transitions.- A.9.1 assert_no_transition.- A.9.2 assert transition.- Appendix B PSL Property Specification Language..- B.1 Introduction to PSL.- B.2 Operators and keywords.- B.3 PSL Boolean layer.- B.4 PSL Temporal Layer.- B.4.1 Named SERE.- B.4.2 SERE concatenation (;) operator.- B.4.3 Consecutive repetition ([*]) operator.- B.4.4 Nonconsecutive repetition ([=]) operator.- B.4.5 Goto repetition ([->]) operator.- B.4.6 Sequence fusion (:) operator.- B.4.7 Sequence non-length-matching (&) operator.- B.4.8 Sequence length-matching (&) operator.- B.4.9 Sequence or (I) operator.- B.4.10 until* sequence operators.- B.4.11 within* sequence operators.- B.4.12 next operator.- B.4.13 eventually! operator.- B.4.14 before* operators.- B.4.15 abort operator.- B.4.16 Endpoint declaration.- B.4.17 Suffix implication operators.- B.4.18 Logical implication operator.- B.4.19 always temporal operator.- B.4.20 never temporal operator.- B.5 PSL properties.- B.5.1 Property declaration.- B.5.2 Named properties.- B.5.3 Property clocking.- B.5.4 forall property replication.- B.6 The verification layer.- B.6.1 assert directive.- B.6.2 assume directive.- B.6.3 cover directive.- B.7 The modeling layer.- B.7.1 rose() and fell() functions.- B.7.2 prey() and next() functions.- B.8 BNF.- B.8.1 Verilog Extensions.- B.8.2 Flavor macros.- B.8.3 Syntax productions.- Appendix C SystemVerilog Assertions.- C.1. Introduction to SystemVerilog.- C.2 Operator and keywords.- C.3 Sequence and property operations.- C.3.1 Temporal delay.- C.3.2 Consecutive repetition.- C.3.3 Goto repetition.- C.3.4 Nonconsecutive repetition.- C.3.5 Sequence and.- C.3.6 Sequence intersection.- C.3.7 Sequence or.- C.3.8 Boolean until (throughout).- C.3.9 Within sequence.- C.3.10 Ended.- C.3.11 Matched.- C.3.12 First match.- C.3.13 Implication.- C.4 Sequences and properties.- C.5 Assert and cover statements..- C.6 Dynamic data within sequences.- C.7 Templates.- C.8 System Functions.- C.9 SystemTasks.- C.10 BNF.- C.10.1 Use of Assertions BNF:.- C.10.2 Assertion statements.- C.10.3 Property and sequence declarations.- C.10.4 Property construction.- C.10.5 Sequence construction.
Recenzii
"By combining its three authors' extensive experience in engineering, applying, and standardizing assertions, this book provides a solid foundation for assertion-based logic design quality and productivity. It is mandatory reading by all computing product design teams. Teams that don't read and apply the assertion-based design ideas in this book will flunk out of the competition."
(Lionel Bening, Hewlett-Packard - Co-Author of "Principles of Verifiable RTL Design")
(Lionel Bening, Hewlett-Packard - Co-Author of "Principles of Verifiable RTL Design")