Computer Hardware Description Languages and their Applications (eBook)

Proceedings of the IFIP WG 10.2 Tenth International Symposium on Computer Hardware Description Languages and their Applications, Marseille, France, 22-24 April 1991

D. Borrione, R. Waxman (Herausgeber)

eBook Download: PDF

2014 | 1. Auflage
490 Seiten
Elsevier Science (Verlag)
978-1-4832-9845-0 (ISBN)

Infos

The topic areas presented within this volume focus on design environments and the applications of hardware description and modelling - including simulation, verification by correctness proofs, synthesis and test. The strong relationship between the topics of CHDL'91 and the work around the use and re-standardization of the VHDL language is also explored. The quality of this proceedings, and its significance to the academic and professional worlds is assured by the excellent technical programme here compiled.

Inhalt

Front Cover 1
Computer Hardware Description Languages and their Applications 4
Copyright Page 5
Table of Contents 10
PREFACE 6
Chapter 1. SOME ISSUES IN HDL–BASED BEHAVIOR MODELLING 14
1 Introduction 14
2 Basic Notions of HDL-based Bahavior Modelling 15
3 Delay Modelling in HDL's 17
4 Support of Register Transfer (RT) Level Descriptions 21
5 Acceptance and Applicability of Broadband Languages 31
6 References 32
Chapter 2. 
34 
I. INTRODUCTION 34
II. THE HARDWARE DESCRIPTION LANGUAGE "CASCADE" 35
III. THE PROOF SYSTEMS 38
IV. COMBINATIONAL CIRCUITS 41
V. SEQUENTIAL DEVICES WITHOUT FEED-BACK LOOPS 42
VI. SEQUENTIAL CIRCUITS WITH FEED-BACK LOOPS 45
VII. REGULAR REPETITIVE DEVICES 47
VIII. CONCLUSION 52
ACKNOWLEDGEMENTS 52
REFERENCES 52
Chapter 3. 
56 
1. INTRODUCTION 56
2. DEFINITION OF THE TRIO LANGUAGE 57
3. TRIO AS A HARDWARE DESCRIPTION LANGUAGE 62
4. AN EXAMPLE: THE CHECKSUM GENERATOR 65
5. A COMPARISON BETWEEN TRIO AND OTHER HDL 71
6. CONCLUDING REMARKS 72
REFERENCES 73
Chapter 4. 
76 
I - INTRODUCTION 76
II - THE DESIGN PROCESS 77
Ill - THE CORRECTNESS PROOF 79
IV - PROVING IN HOL 88
V - THEOREM PROVING 93
VI - CONCLUSIONS 94
VII - ACKNOWLEDGEMENTS 94
Bibliography 95
Chapter 5. 
96 
1 INTRODUCTION 96
2 THE UNTIMED MODEL 98
3 TIMING OF THE PERIPHERY 100
4 MODEL TOLERANCE 101
5 TIMING ANNOTATION STYLES 101
6 SOME EXPERIMENTS 103
7 DISCUSSION 106
ACKNOWLEDGEMENTS 108
References 108
Chapter 6. 
110 
1. INTRODUCTION 110
2. NOTATIONS 111
3. OPEN GATE DISCHARGING 112
4. LOAD DEPENDENT TIMING 116
5. A COMPLETE EXAMPLE 123
6. CONCLUSIONS 126
REFERENCES 127
Chapter 7. 
128 
1. Introduction 128
2. The SiCS - an Overview 129
3. Choosing VHDL as a Basis 130
4. The Simulator Configuration Language 131
5. Processing of the VHDL/S Model Description 139
6. From Description to Simulation 140
7. State of the Work and Outlook 141
8. Related Work 141
9. Summary 141
10. 
142 
Chapter 8. 
144 
1. Introduction 144
2 . The Simulation Semantics of VHDL 144
3. Implicit and Explicit Finite State Machines 146
4. The Synthesis Subsets of Behavioral VHDL 147
5. Extraction of Implicit Finite State Machine 148
6. Convergent Redundancy And Its Removal 153
7. Conclusion 154
Bibliography 154
Chapter 9. 
156 
1. INTRODUCTION 156
2. VHDL 157
3. PARAMETERISING SPECIFICATIONS BY TYPES 157
4. PARAMETERISING SPECIFICATIONS BY FUNCTIONS 161
5. FORMAL VERIFICATION 163
6. CONCLUSION 164
References 164
Chapter 10. 
166 
1 Introduction 166
2 Related Work 167
3 Model 168
4 Methodology 168
5 Modeling Sequential Circuit Behavior with ASMs 170
6 Intermediate Form 171
7 Proof System Input 174
8 Conclusions and Future Work 175
References 175
Chapter 11. 
178 
1 Introduction 178
2 Existing Specification Languages 179
3 The SpecCharts Language 180
4 A General Communication Construct 183
5 A Comparison of SpecCharts with the Statemate Approach 184
6 SpecCharts Usefulness for Specification and Synthesis 185
7 Results and Future Work 186
8 Conclusions 187
9 Acknowledgements 187
References 187
Chapter 12. 
188 
1. Introduction 188
2. The redesign problem 189
3. Redesign methods 190
4. Required mechanisms in CHDLs for redesign methods 193
5. Conclusions 195
References 195
Chapter 13. 
198 
INTRODUCTION 198
1. DECLARATIVE LANGUAGES AND THEIR SCOPE 200
2. DECLARATIVE VERSUS PROCEDURAL DESCRIPTIONS 204
3. TOWARDS DECLARATIVE FORMALISMS 212
4. DECLARATIVE FORMALISMS: STILL A LONG WAY TO GO 222
REFERENCES 224
Chapter 14. 
226 
1 Introduction 226
2 An Overview of CIRCAL 227
3 Abstraction Mechanisms in Circal 232
4 Conclusions 239
References 240
Chapter 15. 
242 
1 Introduction 242
2 Back-annotation with clock statements 245
3 Formal semantics of clocked algorithmic specifications 247
4 Example 251
5 Conclusion 255
References 257
Chapter 16. 
262 
1 INTRODUCTION 262
2 VERIFICATION OF SYNCHRONOUS CIRCUITS 263
3 FIXPOINT ITERATION ALGORITHM 265
4 EMPIRICAL RESULTS 268
5 CONCLUSION 270
A Appendix 271
References 272
Chapter 17. 
274 
1. INTRODUCTION 274
2. REQUIREMENTS FOR TIMING SPECIFICATION 276
3. EXISTING APPROACHES TO TIMING SPECIFICATION 278
4. A NEW MODEL FOR TIMING SPECIFICATION 280
5. TOOLS 288
6. CONCLUSION 291
ACKNOWLEDGEMENTS 291
REFERENCES 292
Chapter 18. 
294 
1. INTRODUCTION 294
2. TIMED PETRI NETS 296
3. USING ER NETS FOR HARDWARE DESCRIPTION: A CASE STUDY 303
4. GENERAL MODELLING RULES 307
5. CONCLUDING REMARKS 311
6. REFERENCES 311
Chapter 19. An Object-Oriented Framework Supporting the full High-Level Synthesis Trajectory 314
1 Introduction 314
2 System overview 316
3 Related work 319
4 The DSFG behavioural kernel 320
5 Library kernel for high-level synthesis 325
6 Conclusions 331
References 332
Chapter 20. Experience in Designing Formally Verifiable HDL's 334
1. Introduction 334
2. Semantics of HDL's 336
3. Support of Modeling Concepts 338
4. Multi-Level Modeling 340
5. Equivalence of expressions 342
6. Support of Divide-and-Conquer 345
7. Conclusions 346
References 347
Chapter 21. 
348 
1. BACKGROUND 348
2. DESIGN LANGUAGE NEEDS AS DISTINCT FROM MODELLING LANGUAGES 349
3. ENCAPSULATIONS: STATE MACHINES AND SYNCHRONOUS LOGIC AS THE STRUCTURED PROGRAMMING OF DIGITAL HARDWARE DESIGN 351
4. EXAMPLE CONSTRUCTS FOR A VHDL EXTENSION FOR SYNTHESIS 353
5. CONCLUSIONS 362
6. REFERENCES 362
Chapter 22. Hierarchical Action Refinement: A Methodology for Compiling Asynchronous Circuits from a Concurrent HDL 364
1 Introduction 364
2 Definition and Informal Semantics of hopCP 366
3 Architecture of the Action Refinement based Compiler 369
4 Synthesis of an Asynchronous LRU circuit 377
5 Conclusions and Future Work 380
References 381
Chapter 23. EDISYN: A Language-Based Editor for High-level Synthesis 384
1 Introduction 384
2 Features of EDISYN 386
3 Implementation of EDISYN 392
4 Generating Code with EDISYN 394
5 Generating Controller and Datapath Descriptions 397
6 Discussion 399
References 401
Chapter 24. 
404 
1 Introduction 404
2 The Specification and Manipulation of Constraints 406
3 The Version Management 411
4 The Module Selection 413
5 Implementation 417
6 Conclusion 418
References 418
Chapter 25. 
420 
1. Problem Description and Contributions 420
2. Previous Work 422
3. The User Interface and Intermediate Representation 423
4. Issues in Behavioral Modeling of Complex Designs 426
5. Outline of Translation Algorithm 434
6. Experiments 434
7. Status 436
8. Summary 437
9. Acknowledgements 437
10. References 437
Chapter 26. 
440 
1. Introduction 440
2. Effects of Event-driven Simulation on Test Generation 441
3. Generation of Realistic Tests 448
4. Bus Resolution Function vs. Test Generation 454
5. Conclusions 456
References 457
Chapter 27. 
458 
1. INTRODUCTION 458
2 . TRANSLATION FROM VHDL TO A N EXPRESSION TREE ISOMORPHIC 
460 
3. DEPENDENCY ANALYSIS 463
4. SIMPLIFICATIONS WITH RESPECT TO THE OPERATORS THEORY 467
5. EXPRESSIONS IDENTIFICATION 468
6. REDUCTION PHASE WITH RESPECT TO THE INFORMATION QUANTITY 472
7. IMPLEMENTATION 474
CONCLUSION 474
REFERENCES 476
Chapter 28. 
478 
1. INTRODUCTION 478
2. RELATED WORK 479
3. DESCRIBING HARDWARE AS A SOFTWARE MODEL 480
4. DERIVING A TEST 482
5. SUMMARY AND OUTLOOK 489
6. ACKNOWLEDGEMENTS 489
7. REFERENCES 489

Produkt-Details

• Erscheint lt. Verlag: 28.6.2014
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Betriebssysteme / Server
• Themenwelt: Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• Themenwelt: Technik ► Maschinenbau
• ISBN-10: 1-4832-9845-0 / 1483298450
• ISBN-13: 978-1-4832-9845-0 / 9781483298450