Practical Formal Methods for Hardware Design

ISBN-13: 9783540620075 / Angielski / Miękka / 1997 / 293 str.

C. Delgado Kloos; Carlos Delgado Kloos; Werner Damm

Opis

This Esprit volume presents research results from the FORMAT (formal methods in hardware verification) project, a collaboration of five European enterprises, a research institute, and two universities.

Spis treści

1. Formal methods vs. conventional ones.- 2. The FORMAT project.- 3. Organization of this book.- I. Overview.- Design Methodology for Complex VLSI Devices.- 1. Introduction: needs and constraints of the ESDA market.- 2. The design flow.- 2.1 Design specification and documentation.- 2.2 VHDL for simulation and synthesis.- 2.3 From specification to implementation.- 3. Design capture with VHDL/S.- 4. The Format methodology at work.- 5. Concluding remarks.- Specification Languages.- 1. VHDL/S.- 2. State based specifications.- 2.1 Integration.- 2.2 A design situation.- 3. Timing diagrams.- 3.1 Syntax definition.- 3.2 Informal semantics.- 4. Example: a traffic light system.- 4.1 Structure of the traffic light system.- 4.2 Behavioural description of the traffic light system.- 5. Timing diagram description.- 6. Summary.- Verification Flow.- 1. Verification tools.- 2. Proof manager.- 2.1 Purpose of the proof manager.- 2.2 Verification of behavioural descriptions.- 2.3 Handling hierarchical structures.- 3. Proof steps for the traffic light system.- 4. Compositional verification.- 5. Component verification.- 5.1 Introduction.- 5.2 Verification of the traffic light controller.- 6. Generation of temporal logic.- 7. Summary.- Synthesis Flow.- 1. Introduction.- 2. Design flow.- 3. Timing diagrams as specifications.- 4. T-LOTOS semantics of timing diagrams.- 4.1 Formalization of timing diagram specifications.- 4.2 Timed graphs as internal representation.- 5. The different ways of producing T-LOTOS implementation descriptions.- 5.1 Automatic transformation.- 5.2 Interactive transformation.- 6. Translation from T-LOTOS to VHDL.- 6.1 Translation process.- 6.2 VHDL produced.- 7. Conclusion.- II. Industrial Experience.- Application of a Formal Verification Toolset to the Design of Integrated Circuits in an Industrial Environment.- 1. Introduction.- 2. Description of the DEPTH circuit.- 2.1 DEPTH interface with the environment.- 2.2 Architecture.- 2.3 Considerations and decisions regarding FORMAT.- 3. Integration of the FORMAT tools into the Telefónica I+D design process.- 3.1 System specification.- 3.2 Synthesis tools.- 3.3 Verification tools.- 4. Working methodology and results.- 4.1 The synthesis line.- 4.2 The verification line.- 5. Conclusions.- Italtel Application of the FORMAT Design Flow.- 1. Introduction.- 2. Device specification in VHDL/S.- 2.1 Design capture.- 3. The verification flow.- 3.1 Design properties.- 3.2 Users’ feedback.- 4. The synthesis flow.- 4.1 From timing diagrams to VHDL.- 4.2 Using the structurizer.- 5. Example of FORMAT tools encapsulation into a framework.- 6. Conclusion.- Siemens Industrial Experience.- 1. Design flow and verification methodology.- 2. Application reports.- 2.1 Verification of a token ring controller.- 2.2 Verification of an arbiter.- 2.3 Verification of a serial V24 interface controller.- 2.4 Verification of an ATM component.- 2.5 Verification of a FIFO buffer component.- 3. Conclusion.- III. Technical Background.- The FORMAT Model Checker.- 1. Introduction.- 2. Architecture.- 2.1 Interfaces.- 2.2 The algorithm.- 3. The checking component.- 4. The debugging component.- 5. The tautology checker.- Reasoning.- 1. LAMBDA — a behavioural design tool.- 1.1 The LAMBDA logic.- 1.2 Proof in LAMBDA.- 2. Generating L2 specifications.- 2.1 Modelling VHDL in L2.- 3. Tutorial examples.- 3.1 Simple reasoning.- 3.2 Recursive definitions.- 3.3 Arrays.- 4. Conclusions.- VHDL Formal Modeling and Analysis.- 1. Introduction.- 2. A formal model of VHDL.- 3. Petri Nets and VHDL analysis.- 3.1 Petri Net analysis.- 3.2 Motivation of structural analysis techniques.- 3.3 VHDL analysis.- 4. Conclusions.- Synthesis Techniques.- 1. Introduction.- 2. T-LOTOS.- 2.1 Syntax of T-LOTOS.- 2.2 T-LOTOS operational semantics.- 2.3 Examples of specifications in T-LOTOS.- 2.4 Timed graphs as internal representation.- 3. Formalizing timing diagrams.- 3.1 General translation approach.- 3.2 Translation of graphical primitives.- 3.3 The operational model.- 4. Automatic synthesis.- 5. Interactive synthesis.- 5.1 The synthesis algorithm.- 5.2 Implementation relation.- 5.3 Protocol conversion.- 5.4 An example: a frequency counter.- 6. Conclusions.- Generating VHDL Code from LOTOS Descriptions.- 1. Introduction.- 2. Translation of T-LOTOS to VHDL.- 2.1 Relation between LOTOS and VHDL semantic elements.- 2.2 Restrictions imposed by the translation.- 2.3 Translation scheme.- 2.4 Optimizing the code.- 3. Design of an ethernet bridge.- 4. System testing.- 4.1 Derivation and validation of test cases.- 4.2 Test suite application.- 5. Testing environment.- 5.1 Test case production.- 5.2 Test cases implementation.- 5.3 Test case execution and report production.- 6. Conclusion.