Practical Formal Methods for Hardware Design (Research Reports Esprit. Project 6128, Format, Vol 1)

Formal methods for hardware design still find limited use in industry. Yet current practice has to change to cope with decreasing design times and increasing quality requirements. This research report presents results from the Esprit project FORMAT (formal methods in hardware verification) which involved the collaboration of the enterprises Siemens, Italtel, Telefonica I+D, TGI, and AHL, the research institute OFFIS, and the universities of Madrid and Passau. The work presented involves advanced specification languages for hardware design that are intuitive to the designer, like timing diagrams and state based languages, as well as their relation to VHDL and formal languages like temporal logic and a process-algebraic calculus. The results of experimental tests of the tools are also presented.

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.