| 000 -LEADER |
|---|
| fixed length control field |
04425nam a22005895i 4500 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| ISBN |
9783540706557 |
| -- |
978-3-540-70655-7 |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
005.18 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Correct Hardware Design and Verification Methods |
| Sub Title |
IFIPWG10.2 Advanced Research Working Conference, CHARME'93 Arles France May 24–26, 1993 Proceedings / |
| Statement of responsibility, etc |
edited by George J. Milne, Laurence Pierre. |
| 260 #1 - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication |
Berlin, Heidelberg : |
| Name of publisher |
Springer Berlin Heidelberg, |
| Year of publication |
1993. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Number of Pages |
IX, 275 p. |
| Other physical details |
online resource. |
| 490 1# - SERIES STATEMENT |
|---|
| Series statement |
Lecture Notes in Computer Science, |
| 505 0# - FORMATTED CONTENTS NOTE |
|---|
| Formatted contents note |
A graph-based method for timing diagrams representation and verification -- A Petri Net approach for the analysis of VHDL descriptions -- Temporal analysis of time bounded digital systems -- Strongly-typed theory of structures and behaviours -- Verification and diagnosis of digital systems by ternary reasoning -- Logic verification of incomplete functions and design error location -- A methodology for system-level design for verifiability -- Algebraic models and the correctness of microprocessors -- Combining symbolic evaluation and object oriented approach for verifying processor-like architectures at the RT-level -- A theory of generic interpreters -- Towards verifying large(r) systems: A strategy and an experiment -- Advancements in symbolic traversal techniques -- Automatic verification of speed-independent circuit designs using the Circal system -- Correct compilation of specifications to deterministic asynchronous circuits -- DDD-FM9001: Derivation of a verified microprocessor -- Calculational derivation of a counter with bounded response time -- Towards a provably correct hardware implementation of occam -- Rewriting with constraints in T-ruby -- Embedding hardware verification within a commercial design framework -- An approach to formalization of data flow graphs. |
| 520 ## - SUMMARY, ETC. |
|---|
| Summary, etc |
These proceedings contain the papers presented at the Advanced Research Working Conference on Correct Hardware Design Methodologies, held in Arles, France, in May 1993, and organized by the ESPRIT Working Group 6018 CHARME-2and the Universit de Provence, Marseille, in cooperation with IFIP Working Group 10.2. Formal verification is emerging as a plausible alternative to exhaustive simulation for establishing correct digital hardware designs. The validation of functional and timing behavior is a major bottleneck in current VLSI design systems, slowing the arrival of products in the marketplace with its associated increase in cost. From being a predominantly academic area of study until a few years ago, formal design and verification techniques are now beginning to migrate into industrial use. As we are now witnessing an increase in activity in this area in both academia and industry, the aim of this working conference was to bring together researchers and users from both communities. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Microprogramming. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Memory management (Computer science). |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Data transmission systems. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Logic design. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Electronics. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Computer Science. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Control Structures and Microprogramming. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Arithmetic and Logic Structures. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Memory Structures. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Input/Output and Data Communications. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Logic Design. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical Term |
Electronics and Microelectronics, Instrumentation. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Milne, George J. |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Pierre, Laurence. |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Uniform Resource Identifier |
http://dx.doi.org/10.1007/BFb0021709 |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) |
|---|
| Koha item type |
E-BOOKS |
| 264 #1 - |
|---|
| -- |
Berlin, Heidelberg : |
| -- |
Springer Berlin Heidelberg, |
| -- |
1993. |
| 336 ## - |
|---|
| -- |
text |
| -- |
txt |
| -- |
rdacontent |
| 337 ## - |
|---|
| -- |
computer |
| -- |
c |
| -- |
rdamedia |
| 338 ## - |
|---|
| -- |
online resource |
| -- |
cr |
| -- |
rdacarrier |
| 347 ## - |
|---|
| -- |
text file |
| -- |
PDF |
| -- |
rda |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE |
|---|
| -- |
0302-9743 ; |
