Correct Hardware Design and Verification Methods

1. Front Matter

   PDF

2. A graph-based method for timing diagrams representation and verification

   • Viktor Cingel

   Pages 1-14

3. A Petri Net approach for the analysis of VHDL descriptions

   • S. Olcoz, J. M. Colom

   Pages 15-26

4. Temporal analysis of time bounded digital systems

   • Alan R. Martello, Steven P. Levitan

   Pages 27-38

5. Strongly-typed theory of structures and behaviours

   • Keith Hanna, Neil Daeche

   Pages 39-54

6. Verification and diagnosis of digital systems by ternary reasoning

   • Ayman M. Wahba, Einar J. Aas

   Pages 55-67

7. Logic verification of incomplete functions and design error location

   • Qinhai Zhang, Charles Trullemans

   Pages 68-79

8. A methodology for system-level design for verifiability

   • Paolo Camurati, Fulvio Corno, Paolo Prinetto

   Pages 80-91

9. Algebraic models and the correctness of microprocessors

   • N. A. Harman, J. V. Tucker

   Pages 92-108

10. Combining symbolic evaluation and object oriented approach for verifying processor-like architectures at the RT-level

    • Jacques Chazarain, Hélne Collavizza

    Pages 109-121

11. A theory of generic interpreters

    • Phillip J. Windley

    Pages 122-134

12. Towards verifying large(r) systems: A strategy and an experiment

    • P. A. Subrahmanyam

    Pages 135-154

13. Advancements in symbolic traversal techniques

    • Gianpiero Cabodi, Paolo Camurati

    Pages 155-166

14. Automatic verification of speed-independent circuit designs using the Circal system

    • Andrew Bailey

    Pages 167-178

15. Correct compilation of specifications to deterministic asynchronous circuits

    • Scott F. Smith, Amy E. Zwarico

    Pages 179-190

16. DDD-FM9001: Derivation of a verified microprocessor

    • Bhaskar Bose, Steven D. Johnson

    Pages 191-202

17. Calculational derivation of a counter with bounded response time

    • Joep L. W. Kessels

    Pages 203-213

18. Towards a provably correct hardware implementation of occam

    • He Jifeng, Ian Page, Jonathan Bowen

    Pages 214-225

19. Rewriting with constraints in T-ruby

    • Robin Sharp, Ole Rasmussen

    Pages 226-241

20. Embedding hardware verification within a commercial design framework

    • Thomas Kropf, Ramayya Kumar, Klaus Schneider

    Pages 242-257

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.

• Circuit Design
• Circuit Verification
• Correct Hardware Design
• Correct Hardware Verification
• DOM
• Formal Methods
• Formale Methoden
• Korrekte Hardware-Verifikation
• Korrekter Hardware-Entwurf
• Schaltkreisverifikation
• VLSI
• formal verification

Policies and ethics