دانلود کتاب Prospects for Hardware Foundations: ESPRIT Working Group 8533 NADA ― New Hardware Design Methods Survey Chapters (Lecture Notes in Computer Science, 1546)

فهرست مطالب :

Prospects for Hardware Foundations
Preface
Table of Contents
Introduction: NADA and NIL
A Survey of Esprit Working Group 8533 NADA - New Hardware Design Methods
1.1 Aims and Scope
1.2 The NADA Participants
1.3 Main Overall Achievements
1.4 Workshops and Conferences
Project Achievements of the Individual Sites
Observations on NIL - The NADA Integrated
Introduction
Central Requirements on NIL
Survey of NIL Core Concepts
Reasoning
Survey of the Chapters of the Book
Mathematical Foundations
Hardware and Dynamical Systems
Verification and Deductive Design
References
Streams, Stream Transformers and Domain Representations
Introduction
Background
Domain representations of streams and stream transformers
Basic properties of streams and stream transformers
General definitions
Some examples of streams and stream transformers
Time transformations
State transformations
The analogue to digital converter
DA-conversion or curve fitting
Signal transformations
Domains
Preliminaries on domains
Effective domains
Domain representability
Basic definitions
Standard representations of metric spaces
Representing relations and non-continuous functions
Modelling streams
Modelling stream transformers
Transformations of continuous streams
Simple transformations of non-continuous streams
Concluding remarks
References
Ideal Stream Algebra
Origin and Goals
Streams and Ideals
A Simple Soda Machine
Fairness
Channels
Two Stream Based Models of Systems
Modules as Stream Processing Functions
Trace Models
Mathematical Background
Order Theoretic Preliminaries
Pointwise Extension
Directed Sets and the Ideal Completion
Streams as Ideals
Setting for Non Interleaving Semantics
Behaviours and Refinement
Describing Behaviours by Properties
Maximal and In nite Ideals
Maximal Ideals
Infinite Ideals
Refinement Laws
An Alternative Characterisation of Infinite Ideals
About max-Determinedness
Streams and Properties
Maximal and Infinite Streams
Stream Concatenation
Infinite Repetition
Streams of Functions
Feedback and State Based Systems
The Feedback Operation
State Based Systems and Automata
Processes and Synchronised Parallel Composition
Safety
Definition and Topological Properties
Safety and Snapshot sets
Continual Satisfaction
The General Case
Deriving a Recursion for saf
Liveness
Definition and Topological Properties
Liveness and Snapshot Sets
Spanning Infinite Behaviours by Snapshot Sets
Specification of a Bounded Buffer
Transformation to Automaton Form
Counting Resumed
Decomposition
The One Place Buffer
From Buffers to Queues
Conclusion
References
Appendix: Auxiliary Lemmas
Cones and Maximal Elements
Directed Sets
Normalization by Evaluation
Introduction
A simply typed lambda-calculus with constants
Types and terms; rewrite rules
Examples
Normalizable terms and their normal forms
Term families
Domain theoretic semantics of simply typed lambda-calculi
Normalization by evaluation
Reification and reflection; interpretation of the constants
Special rewrite rules
Comparison
Related work
Comparison of algorithms
References
Algebraic Models of Superscalar Microprocessor Implementations: A Case Study
Introduction
Basic Models of Microprocessors
Simple Correctness Models
Retimings
Correctness Statement
Superscalar Microprocessors
Superscalar Correctness
PM: A Simple Architecture
ACS: An Informal Description
Processor Organisation
Processor Operations
ACS: A Formal Description
The State Algebra
Processor Initialisation and Next-State Functions
Processor Operations
Correctness and Verification
A Correctness Definition for ACS
Verifying ACS
Concluding Remarks
References
Hierarchies of Spatially Extended Systems and Synchronous Concurrent Algorithms
Introduction
Spatially Extended Systems
Spatially Extended Deterministic Systems
A Classification of Spatially Extended Systems
Examples
Computability and Equational Specification of Spatially Extended Systems
Modelling Systems
Equational Specification of Computable Data Types
Systems as Data Types
Abstraction and Approximation Between Spatially Extended Deterministic Systems
Abstractions of Components
Abstraction and Approximation of Behaviour
Synchronous Concurrent Algorithms
Formal Definition
SCAs as Spatially Extended Systems
Example: Systolic Convolver
Example: Model of Cardiac Tissue
Abstraction and Approximation Between SCAs
Comparing Components of SCAs
Notions of Abstraction and Approximation for SCAs
Example: Abstraction Between Systolic Convolvers
Example: Approximation Between Models of Cardiac Tissue
Concluding Remarks
References
Towards an Algebraic Specification of the Java Virtual Machine
Introduction
Modelling and Specification Preliminaries
Machine Semantics
Machine States
Specification Framework
An Abstract Model of the JVM
Overview of the JVM
Abstraction
Architectural Specification
Abstract Instructions
Semantics of the Abstract JVM
The Operand Stack
The Local Variables
The Execution Environment
Frames
Registers
Single Threads
The Method Area
The Heap
Modelling the Concrete JVM
The Underlying Data Structures
Dealing with the Remaining Simplifications
Conclusions
References
Grid Protocol Specifications
Introduction
Data and some Process Algebra
Actions, Value-Passing, and Generalized Merge
Parallel Input: Early Reads and Process Prefix
Modules and Connected, single-I/O Networks
Modules
Connected Networks
Characterization of Connected, Single-I/O Networks
Beating Grid Protocols
Synchronized Modules
Networks with a Beat
Characterization of Beating Grid Protocols
An Example: the Wave Equation
The wave equation
Grid Protocols modeling the Wave
Conclusions
References
Appendix
The Computational Description of Analogue System Behaviour
Introduction
A Computational Approach
Language
Semantic Domains
Logic
Semantic Functions
Approximation
Experiments
Conclusion
References
Reasoning about Imperfect Digital Systems
Introduction
Analog specifications
Examples (static specifications)
Examples (dynamic specifications)
Operations on specifications
Correctness
Rectilinear specifications
Examples
Specification at the digital level
Analog level behaviours
Specification at the analog level
Implementation at the analog level
Verification at the analog level
Decision procedure
Practical implementation
Conclusions
Acknowledgments
References
Appendix
Formal Verification and Hardware Design with Statecharts
Introduction
Introduction to mu-Charts
Motivation
Example
Syntax
Sequential Automata
Parallel Composition
Broadcast Communication
Hierarchical Decomposition
Semantics
Transition Semantics
Preliminaries
Configurations
Sequential Automata
Parallel Composition
Hierarchical Decomposition
Broadcast Communication
Formal Verification
The Verifier mu-cke
Encoding
Model Checking
Hardware Generation
Symbolic Encoding of mu-Charts
Stopwatch Example
Conclusion
References
An Exercise in Conditional Refinement
Introduction
Basic Concepts and Notations
Specification of a FIFO Queue
Time Independent Specification
Time Synchronous Specification
Composite Specification
Refinement
Schematic Translation into Time Dependent Format
Semantics of Elementary Time Dependent Specifications
Semantics of Composite Time Dependent Specifications
Two Concepts of Conditional Refinement
Correctness of the FIFO Decomposition
Imposing Additional Boundedness Constraints
Hardware Queue
Interface Component
Software Queue
Composite Specification
Conclusions
Acknowledgements
References
A: Three Rules
Transitivity Rule
Modularity Rule
Decomposition Rule
B: Soundness of Rules
Transitivity Rule
Modularity Rule
Decomposition Rule
Deductive Hardware Design: A Functional Approach
Introduction
Deductive Design
The Framework
Part I: Combinational Circuits
A Model of Combinational Circuits
Functions as Modules
Modelling Connections
Wire Bundles
Numbers and Their Representation
Development of an Adder
The Unfold/Fold Strategy
Generalisation
Modularisation
Abstraction
Re-Use of a Design: Successor (Counting)
Specialisation: Base 2
The Carry Lookahead Adder and Hybrid Adders
More About Wiring
Basic Wiring Elements
Sequential and Parallel Composition
Basic Laws (Network Algebra I)
Selection
Recursions for the Bundle Operations
Combinator Abstraction
A Further Example: Shuffling
Part II: Sequential Hardware
A Model of Streams
Networks
Lifting and Constant
Initialised Unit Delay
Example: The Single Pulser
Formal Specification
Derivation of a Pulser Circuit
Feedback
The Feedback Operation
Properties of Feedback (Network Algebra II)
Interconnection (Mutual Feedback)
A Convolver
Specification
About Error Handling
Derivation of a Convolver Circuit
Unwinding the recursion
Towards a Systolic Version
Speedup by Slowdown
Interleaved Streams
The Slowdown Function
Slowdown Algebra
A Systolic Convolver: The 2-Slow Convolver
Pipelining
Conclusion
References
Appendix: Essential Constructs of Haskell