Computer Hardware Description Languages and their Applications (eBook)

Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL '93 Sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993

D. Agnew, R. Camposano, L. Claesen (Herausgeber)

eBook Download: PDF

2014 | 1. Auflage
618 Seiten
Elsevier Science (Verlag)
978-1-4832-9802-3 (ISBN)

Infos

Hardware description languages (HDLs) have established themselves as one of the principal means of designing electronic systems. The interest in and usage of HDLs continues to spread rapidly, driven by the increasing complexity of systems, the growth of HDL-driven synthesis, the research on formal design methods and many other related advances.This research-oriented publication aims to make a strong contribution to further developments in the field. The following topics are explored in depth: BDD-based system design and analysis; system level formal verification; formal reasoning on hardware; languages for protocol specification; VHDL; HDL-based design methods; high level synthesis; and text/graphical HDLs. There are short papers covering advanced design capture and recent work in high level synthesis and formal verification. In addition, several invited presentations on key issues discuss and summarize recent advances in real time system design, automatic verification of sequential circuits and languages for protocol specification.

Inhalt

Front Cover 1
Computer Hardware Description Languages and Their Applications 4
Copyright Page 5
Table of Contents 15
Preface 6
Conference Organization 8
"Real Time Distributed Systems (invited presentation)" Mario R. Barbacci, Carnegie Mellon University 16
Real-time Distributed Systems 18
1. Introduction 18
2. Industrial Computing Applications 18
3. The Real-Time Distributed Systems Program at the SEI 19
4. A Science and Technology Maturity Model 23
5. An Industrial Computing Developers Handbook 24
Session : BDD-based Design and Analysis Techniques chair: Luc Claesen 28
Verification of the Futurebus+ Cache Coherence Protocol* 30
1. INTRODUCTION 31
2. TEMPORAL LOGIC MODEL CHECKING 32
3. SMV 34
4. OVERVIEW OF THE PROTOCOL 37
5. MODELING THE PROTOCOL 39
6. SPECIFYING CACHE COHERENCE 40
7. SOME ERRORS FOUND DURING VERIFICATION 42
8. CONCLUSIONS 44
9. ACKNOWLEDGMENTS 45
10. REFERENCES 45
Chapter 03."Exploiting Symbolic Traversal Techniques for Efficient Process Algebra Manipulation" 46
1 Introduction 46
2 The rationale of Process Algebras 47
3 Symbolic Traversal Techniques 50
4 Symbolic Generation of Process Algebra Agents 51
5 Experimental Results 55
6 Conclusions 56
References 57
Chapter 04."Hardware- Verification using First Order BDDs " 60
1 Introduction 60
2 First Order BDD-like Calculi 61
3 A Hierarchical Hardware Case Study 71
4 Experimental Results 75
5 Summary 76
References 77
Session: HDL-based Design Methods chair: Franz Rammig 78
Chapter 05."HW/SW Co-Design with PRAMs Using CoDES" 80
1. Introduction 80
2. Parallel Random Access Machines 81
3. System Overview 83
4. Principal Design Steps 84
5. Example 89
6. Conclusion and Future Work 91
7. References 92
Chapter 06."Prevail-DM: A Framework-Based Environment for Formal Hardware Verification " 94
1 INTRODUCTION 94
2 INTRODUCTION TO PREVAIL 96
3 OVERVIEW OF PREVAIL-DM 96
4 CONCEPTUAL SCHEMA 98
5 IMPLEMENTATION ASPECTS 105
6 ANALYSIS OF THE ENVIRONMENT 106
7 DESIGN METHODOLOGY MANAGEMENT 107
8 FINAL REMARKS 109
Acknowledgments 110
References 110
Chapter 07."Better Verification Through Symmetry" 112
1 Introduction 112
2 Symmetry and the Murf Verification System 113
3 Better Verification 119
4 Practical Results 123
5 Data saturation 124
6 Conclusion 125
Acknowledgements 125
References 126
Session: Synthesis and Verification chair: Mario Barbacci 128
Chapter 08."A Rewriting Based Method for the Formal Verification of Microprocessors" 130
1 Introduction 130
2 Overview of the problem 131
3 Implementation of this method 133
4 Applications 135
5 Conclusion 136
References 136
Chapter 09."Reasoning about the VHDL Standard Logic Package Signal Data Type " 138
1 Motivation 138
2 Modeling Signal Values 139
3 Example 142
4 Conclusion 144
5 Acknowledgements 144
References 145
Chapter 10."An Efficient Data-Path Synthesis Based on Algorithmic Description under the Constraints of Time and Area" 146
1. INTRODUCTION 146
2. FINDING REDESIGNING METHODS 147
3. REDESIGN 149
4. EXPERIMENTS 151
5. CONCLUDING REMARKS 152
6. REFERENCES 153
Chapter 11."Integrating Boolean Verification with Formal Derivation" 154
1. Introduction 154
2. DDD - D_igital D_esign D_erivation System 155
3. The DDD-FM9001 Project 157
4. Verification of the DDD-FM9001 ALU 158
5. Concluding Remarks 160
REFERENCES 160
Chapter 12."Automated High-level Verification Against Clocked Algorithmic Specifications" 162
1 Introduction 162
2 Representation 163
3 Algorithm 164
4 Experimental results and future work 166
References 166
Chapter 13."The Backward Walk Approach in FSM Verification" 170
1 Introduction 170
2 Notations and Definitions 171
3 Our Algorithm 172
4 Hopcroft's Algorithm 173
5 Data Structure of the Partition 173
6 Filkorn's Method 174
7 The Detection of Non-reachable States 174
8 Experiments 175
9 Conclusion and Future Work 176
Acknowledgments 177
References 177
Invited Presentation : Automatic Verification of Sequential Circuit Designs Edmund M. Clarke, Carnegie Mellon University 178
Automatic Verification of Sequential Circuit Designs 180
Session: Protocol Specification chair: Ed Cerny 182
Chapter 14."Toward a Basis for Protocol Specification and Process Decomposition " 184
1. Introduction 184
2. A Language for Protocol Specification 186
4. Interpretation 190
5. Relations 
193 
6. An Example of Process Decomposition 197
7. Observations and Conclusion 199
8. Acknowledgements 199
REFERENCES 200
Chapter 15."Integrating SDL and VHDL for System-Level Hardware Design" 202
1 Introduction 202
2 WHAT IS SDL ? 204
3 SDL and Object-Oriented Design of Hardware 205
4 An SDL-Based Hardware Design Environment 208
5 Example 212
6 Conclusions 216
Acknowledgement 217
References 217
Session:Formal Reasoning about Regular Structures 
220 
Chapter 16. Reasoning About Array Structures Using a Dependently Typed Logic 
222 
1 Introduction 222
2 The Veritas Design Logic 224
3 Array Structures 227
4 Systolic Arrays 233
5 Triangular Dependency Graph Example 236
6 Conclusions 238
7 Acknowledgements 239
References 239
Chapter 17."VHDL Description and Formal Verification of Systolic Multipliers" 240
I. INTRODUCTION 240
II. ILLUSTRATIVE EXAMPLE. 241
III. OVERVIEW OF THE BOYER-MOORE SYSTEM. 243
IV. MODELLING SYSTOLIC MULTIPLIERS WITH BOYER-MOORE. 244
V. PROOF METHODOLOGY. 248
VI. GENERALIZING THE SPECIFICATION. 250
VII. A MORE COMPLEX EXAMPLE. 253
VIII . CONCLUSION. 256
ACKNOWLEDGEMENTS 257
REFERENCES 257
Chapter 18.Transformational Rewriting with Ruby 258
1. Introduction 258
2 .The Ruby Language 259
3· Rewriting Ruby Terms 262
4. The Rewrite Process 267
5. Conclusion 274
6. Acknowledgements 274
References 274
Session: High Level Synthesis chair: Flavio Wagner 276
Chapter 19."A Representation for the Binding of RT-Component Functionality to HDL Behavior" 278
1. Introduction 278
2. Related Work 281
3. Representation of Component Functions and Bindings 282
4. Example Application 288
5. Further Examples 292
6. Summary and Future Directions 293
Acknowledgments 294
References 294
Chapter 20."Performance Specification and Measurement" 296
1 Introduction 296
2 An Invitation to PDL 298
3 PDL: The Language 300
4 Advanced features 304
5 Dynamic Attributes 307
6 Compiling PDL 309
7 PDL - VHDL translation 310
8 PDL: Execution Environment 311
9 Results and Future Work 311
10 Acknowledgements 312
References 312
Chapter 21."Automatic Synthesis of Sequential Synchronizations" 314
1 Introduction 314
2 The Specification Language 
316 
3 Specification of Digital Components 322
4 Synchronization Specification and Derivation 324
5 Solving Systems of Inequalities 325
6 Conclusion 329
References 329
Session:Design Capture chair: Edmund M. Clarke 332
Chapter 22."Specifying Hardware Systems in LOTOS" 334
1. Introduction and Background 334
2.Formal Specifications of Small Digital Circuits 335
3. Validating the Specification 339
4. Conclusions and Research Directions 340
References 340
Chapter 23."HML: A Hardware Description Language Based on Standard ML" 342
1 Introduction 342
2 The HML Language 344
3 An Example : A Floating Point Adder 347
4 Conclusion 348
Acknowledgements 349
References 349
Chapter 24."An Efficient Object-Oriented Variation of the Statecharts Formalism for Distributed Real-Time Systems" 350
1. INTRODUCTION 350
2. AN OVERVIEW OF ROOM 351
3. ROOMCHARTS 352
4. INHERITANCE 357
5. RELATED WORK 357
6. EXPERIENCE WITH ROOMCHARTS 358
Acknowledgments 359
7. REFERENCES 359
Chapter 25."Linking System Design Tools and Hardware Design Tools 
360 
1. Introduction 360
2. Previous Work 361
3. COSMOS: Linking The Worlds Of System Design And Circuit Design 362
4. Conclusions And Future Work 365
References 366
Chapter 26."Automatic VHDL Model Generation System" 14
Chapter 27.Automatic VHDL Model Generation System 368
1. INTRODUCTION 368
2. AUTOMATIC VHDL MODEL GENERATION 369
3. PREPROCESSOR AND POSTPROCESSOR 370
4. AUTOMATIC CODE GENERATOR 371
5. AUTOMATIC MODEL CHECKER 373
6. MODEL LIBRARY AND RULE BASE 374
7. RESULTS 374
8. CONCLUSION 374
9. REFERENCES 375
Chapter 28."The Modeler's Assistant: A CAD Tool for Behavioral Model Development" 376
1. THE PROCESS MODEL GRAPH REPRESENTATION 376
2. THE MODELERS ASSISTANT 378
3. REFERENCES 383
Chapter 29."Insulin: An Instruction Set Simulation Environment" 384
1. Introduction 384
2. The Micro-Architecture Design System 385
3. Instruction Set Simulation 386
4. Comparison with Existing Systems 390
5. Conclusion 390
6. References 391
"Specification languages for communication protocols (invited presentation)" 392
Session: Timing Specifications in HDLs chair: John Brzozowski 412
Chapter 30."Integrating Behavior and Timing in Executable Specifications" 414
1 Introduction 414
2 Interface Specifications 416
3 The Timing Diagram Interpreter 421
4 Procedural linking 423
5 A Complete Approach to Modeling 425
6 Discussion 429
7 Conclusion 430
References 431
Chapter 31."ESP: An Executable Specification Language for Mixed Timing Control Circuits " 432
1 Introduction 432
2 Background, Features and Basic Notions 434
3 Semantics of ESP Syntactic Constructs 438
4 Simulation of ESP using Simulation State Graphs 443
5 Partial Specification of the ISA Bus 445
6 Conclusion and Plans for Further Research 447
References 448
Session:Textual and Graphical HDLs chair: Robert Hum 450
Chapter 32."UDL/I version Two: A New Horizon of HDL Standards" 452
1. Introduction 452
2. Requirements for the Standard HDLs 454
3. Design Philosophy of UDL/I Version Two 456
4. Features of UDL/I 457
5. Description example 462
6. UDL/I Committee Current Status and the Future Plan 464
7. Summary 466
Acknowledgments 466
References 467
Chapter 33."Verilog HDL Modeling Styles for Formal Verification" 468
1 INTRODUCTION 469
2 NON-DETERMINISM IN THE VERILOG HDL 469
3 FINITE STATE MACHINE MODELING STYLES 470
4 SELECTION/RESOLUTION MODEL AND L-PROCESSES 471
5 GENERAL MODELING STYLE 474
6 DETERMINISTIC OUTPUT 476
7 DETERMINISTIC TRANSITIONS 477
8 TIMING EXTENSIONS 478
9 CONCLUSION 480
10 REFERENCES 480
Chapter 34."A Visual Hardware Description Language " 482
1 INTRODUCTION 482
2 RELATED WORK 483
3 A VISUAL APPROACH TO HARDWARE DES CRIPTION 484
4 A VISUAL SYNTAX FOR VHDL 487
5 DISCUSSION 494
Acknowledgements 496
References 496
Chapter 35."Textual/Graphical Design Concept-Level Synthesis" 500
INTRODUCTION 500
CONCEPTUAL GRAPHS 501
BLOCK DIAGRAMS 504
TIMING DIAGRAMS 505
STATE TRANSITION DIAGRAMS 507
NATURAL LANGUAGE 508
INTEGRATION AND CONSISTENCY CHECKING 511
SYNTHESIS 515
CONCLUSIONS 516
REFERENCES 517
Sessions : VHDL 518
Chapter 36."System-Level Specification and Design Using VHDL: A Case Study" 520
1 Introduction 520
2 The Causal Level 521
3 Specification and Design of the Processor at the Causal Level 522
4 Optimization Strategies 527
5 RT-level Optimizations of the Design Example 530
6 HW/SW Co - Specification and Co-Design 531
7 Analysis of the Design Example 533
8 Conclusion 535
Acknowledgements 535
References 535
Chapter 37."A Denotational Definition of the VHDL Simulation Kernel" 538
1. Introduction 538
2. Behavioral Modeling in VHDL 539
3 . Modeling the Simulation Kernel 540
4. An Example 546
5. Discussion 549
Acknowledgments 549
6.References 550
Chapter 38."Checking DFT Rules with a VHDL Simulator" 552
1 Introduction 552
2 Basic Principle 553
3 Checking Rules for Synchronous Design 553
4 Checking Rules for Modular Testing Support 558
5 Possible Extensions to Some Other Applications 562
6 Limitations 563
7 Conclusions 564
Acknowledgements 564
References 564
Chapter 39."Parameterized VHDL entities for the simulation of hybrid circuits" 566
1. Introduction 566
2. Signal representation in RAMSES 567
3. Contents of the RAMSES libraries 569
4. Complete example 576
5. Current limitations 581
6. Future work 581
7. Conclusion 582
8. Literature 582
Chapter 40."Modeling Timing Behavior of Logic Circuits Using Piecewise Linear Models" 584
1. INTRODUCTION 584
2. MODELING PRINCIPLE 585
3. MODELING TECHNIQUE 587
4. VHDL IMPLEMENTATION OF GATE MODELS 591
5. PARAMETER EXTRACTION AND SIMULATION 595
6. MODELING EXAMPLE 598
7. CONCLUSIONS 601
REFERENCES 601
Chapter 41."Analog-VHDL: As an application, a real example" 602
I. Introduction 602
II. Synchronization of Algorithms 603
III. The mixed interface 604
IV. MINT-Sugar 605
V. Presentation of analog-VHDL 605
VI. A complete example 610
VIL Conclusion 619
Acknowledgements 619
BIBLIOGRAPHY 619

Produkt-Details

• Erscheint lt. Verlag: 21.5.2014
• Sprache: englisch
• Themenwelt: Mathematik / Informatik ► Informatik ► Betriebssysteme / Server
• Themenwelt: Mathematik / Informatik ► Informatik ► Theorie / Studium
• ISBN-10: 1-4832-9802-7 / 1483298027
• ISBN-13: 978-1-4832-9802-3 / 9781483298023