Correct Hardware Design and Verification Methods
Editat de Tiziana Margaria, Tom Melhamen Limba Engleză Paperback – 27 aug 2001
Preț: 332.18 lei
Preț vechi: 415.23 lei
-20%
Puncte Express: 498
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: 9783540425410
ISBN-10: 3540425411
Pagini: 496
Ilustrații: XII, 488 p.
Dimensiuni: 155 x 235 x 27 mm
Greutate: 0.74 kg
Ediția:2001
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540425411
Pagini: 496
Ilustrații: XII, 488 p.
Dimensiuni: 155 x 235 x 27 mm
Greutate: 0.74 kg
Ediția:2001
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Invited Contributions.- View from the Fringe of the Fringe.- Hardware Synthesis Using SAFL and Application to Processor Design.- FMCAD 2000.- Applications of Hierarchical Verification in Model Checking.- Model Checking 1.- Pruning Techniques for the SAT-Based Bounded Model Checking Problem.- Heuristics for Hierarchical Partitioning with Application to Model Checking.- Short Papers 1.- Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs.- Deriving Real-Time Programs from Duration Calculus Specifications.- Reproducing Synchronization Bugs with Model Checking.- Formally-Based Design Evaluation.- Clocking Issues.- Multiclock Esterel.- Register Transformations with Multiple Clock Domains.- Temporal Properties of Self-Timed Rings.- Short Papers 2.- Coverability Analysis Using Symbolic Model Checking.- Specifying Hardware Timing with ET-Lotos.- Formal Pipeline Design.- Verification of Basic Block Schedules Using RTL Transformations.- Joint Session with TPHOLs.- Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking.- Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider.- Hardware Compilation.- Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques.- A Higher-Level Language for Hardware Synthesis.- Tools.- Hierarchical Verification Using an MDG-HOL Hybrid Tool.- Exploiting Transition Locality in Automatic Verification.- Efficient Debugging in a Formal Verification Environment.- Model Checking 2.- Using Combinatorial Optimization Methods for Quantification Scheduling.- Net Reductions for LTL Model-Checking.- Component Verification.- Formal Verification of the VAMP Floating Point Unit.- A Specification Methodology by a Collection ofCompact Properties as Applied to the Intel® Itanium™ Processor Bus Protocol.- The Design and Verification of a Sorter Core.- Case Studies.- Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip.- Using Abstract Specifications to Verify PowerPC™ Custom Memories by Symbolic Trajectory Evaluation.- Algorithm Verification.- Formal Verification of Conflict Detection Algorithms.- Induction-Oriented Formal Verification in Symmetric Interconnection Networks.- A Framework for Microprocessor Correctness Statements.- Duration Calculus.- From Operational Semantics to Denotational Semantics for Verilog.- Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming.