Kazmierski / Morawiec System Specification and Design Languages

Selected Contributions from FDL 2010
1. Auflage 2011
ISBN: 978-1-4614-1427-8
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 106, 256 Seiten

Reihe: Lecture Notes in Electrical Engineering

This book brings together a selection of the best papers from the thirteenth edition of the Forum on specification and Design Languages Conference (FDL), which was held in Southampton, UK in September 2010.  FDL is a well established international forum devoted to dissemination of research results, practical experiences and new ideas in the application of specification, design and verification languages to the design, modelling and verification of integrated circuits, complex hardware/software embedded systems, and mixed-technology systems.

Autoren/Hrsg.

Morawiec, Adam

Kazmierski, Tom J.

Inhaltsverzeichnis

1;System Specification and Design Languages;3
1.1;Preface;5
1.2;Contents;7
1.3;Contributors;9
1.4;Chapter 1 Formal Hardware/Software Co-verification of Application Specific Instruction Set Processors;13
1.4.1;1.1 Introduction;13
1.4.2;1.2 Interval Property Checking;15
1.4.2.1;1.2.1 Hardware Models and Property Languages;15
1.4.3;1.3 IPC for Weakly Programmable IP;18
1.4.4;1.4 Configuration and Context-Dependent Constraints;21
1.4.4.1;1.4.1 Hazard Detection;22
1.4.5;1.5 Completeness;24
1.4.6;1.6 Hardware/Software Compliance;27
1.4.7;1.7 Applications;28
1.4.8;1.8 Conclusion;31
1.4.9;References;31
1.5;Chapter 2 Evaluating Debugging Algorithms from a Qualitative Perspective;33
1.5.1;2.1 Introduction;33
1.5.2;2.2 Preliminaries;35
1.5.2.1;2.2.1 Faults, Bugs, and Errors;35
1.5.2.2;2.2.2 Computation of CFG and PDG;35
1.5.2.3;2.2.3 Simulation-Based Debugging;36
1.5.3;2.3 General Idea and Discussion;37
1.5.3.1;2.3.1 Qualitative Assessment;38
1.5.3.2;2.3.2 Limits of Quantitative Assessments;38
1.5.4;2.4 Fault Model;39
1.5.4.1;2.4.1 Programming Faults;40
1.5.4.1.1;2.4.1.1 Assignment Fault;40
1.5.4.1.2;2.4.1.2 Operation Fault;40
1.5.4.1.3;2.4.1.3 Incorrect Data/Port Type;41
1.5.4.2;2.4.2 Design Faults;42
1.5.4.2.1;2.4.2.1 Missing Code;42
1.5.4.2.2;2.4.2.2 Extra Code;43
1.5.4.2.3;2.4.2.3 Misplaced Code;44
1.5.4.2.4;2.4.2.4 Signal Binding Faults;44
1.5.5;2.5 Evaluation: Simulation-Based Debugging;45
1.5.5.1;2.5.1 Limitations of Quantitative Analysis;46
1.5.5.2;2.5.2 Qualitative Assessment;46
1.5.6;2.6 Conclusion;47
1.5.7;References;47
1.6;Chapter 3 Mapping of Concurrent Object-Oriented Models to Extended Real-Time Task Networks;49
1.6.1;3.1 Introduction;49
1.6.2;3.2 Modelling Approach;51
1.6.2.1;3.2.1 Executable Model – OSSS Design Methodology;51
1.6.2.2;3.2.2 Analytical/Formal Model;54
1.6.3;3.3 Mapping;57
1.6.3.1;3.3.1 Port-Interface Binding;57
1.6.3.2;3.3.2 Shared Object;58
1.6.3.3;3.3.3 Task Model;59
1.6.4;3.4 Use-Case;60
1.6.4.1;3.4.1 Service Call;60
1.6.4.2;3.4.2 Mutual Exclusion;60
1.6.4.3;3.4.3 Multiplexer with Priority-Based Scheduling;61
1.6.5;3.5 Conclusion and Future Work;64
1.6.6;References;64
1.7;Chapter 4 SystemC-A Modelling of Mixed-Technology Systems with Distributed Behaviour;66
1.7.1;4.1 Introduction;66
1.7.2;4.2 SystemC-A;68
1.7.2.1;4.2.1 Subsection Heading;68
1.7.2.1.1;4.2.1.1 Analogue Components;68
1.7.2.2;4.2.2 Virtual Build Method;69
1.7.3;4.3 Case Study 1: SystemC-A Modelling of Distributed Lossy Transmission Line;69
1.7.3.1;4.3.1 Distributed Model of Lossy Microstrip;69
1.7.3.2;4.3.2 SystemC-A Implementation of Proposed Model;71
1.7.3.3;4.3.3 Simulation Results;73
1.7.4;4.4 Case Study 2: SystemC-A Modelling of the Distributed Cantilever Beam;73
1.7.4.1;4.4.1 SystemC-A Implementation of Cantilever Beam;76
1.7.4.2;4.4.2 Simulation Results;78
1.7.5;4.5 Conclusion;78
1.7.6;References;78
1.8;Chapter 5 A Framework for Interactive Refinement of Mixed HW/SW/Analog Systems;81
1.8.1;5.1 Introduction;82
1.8.2;5.2 Related Work;82
1.8.3;5.3 Synchronisation;83
1.8.3.1;5.3.1 Analogue Events;84
1.8.3.2;5.3.2 Sampled Signals;84
1.8.3.3;5.3.3 Pre-Synchronisation;85
1.8.4;5.4 Usability;86
1.8.4.1;5.4.1 Signal Pool;86
1.8.4.2;5.4.2 SystemC Proxy Module;90
1.8.4.3;5.4.3 Graphical Design Entry;91
1.8.5;5.5 Design Example;93
1.8.5.1;5.5.1 Design Effort;94
1.8.5.2;5.5.2 Performance and Accuracy;95
1.8.6;5.6 Conclusion;97
1.8.7;References;97
1.9;Chapter 6 Bottom-up Verification for CMOS Photonic Linear Heterogeneous System;100
1.9.1;6.1 Introduction;101
1.9.2;6.2 Simulation strategy for heterogeneous cmos photonic system;102
1.9.3;6.3 Model implementation;104
1.9.3.1;6.3.1 Optical passive devices modeling;104
1.9.3.2;6.3.2 Modeling difficulties;107
1.9.3.3;6.3.3 Analysis and solution;107
1.9.3.4;6.3.4 VPI implementation details;109
1.9.4;6.4 Numerical application;109
1.9.5;6.5 Conclusion;111
1.9.6;References;111
1.10;Chapter 7 Towards Abstract Analysis Techniques for Range Based System Simulations;114
1.10.1;7.1 Introduction;115
1.10.2;7.2 Related Work;116
1.10.3;7.3 Semi-Symbolic Simulation Environment;116
1.10.3.1;7.3.1 Affine Arithmetic;117
1.10.3.2;7.3.2 SystemC AMS;118
1.10.3.3;7.3.3 Transistor Level Solver;118
1.10.4;7.4 Enhanced Range Signal Analysis;119
1.10.4.1;7.4.1 Traditional Fourier Transform;120
1.10.4.2;7.4.2 Range Based Fourier Transformation;120
1.10.4.3;7.4.3 Amplitude Frequency Spectrum;122
1.10.4.4;7.4.4 Phase Frequency Spectrum;123
1.10.4.5;7.4.5 Applied Range Based Fourier Transform;123
1.10.4.6;7.4.6 Runtime of Range Based Fourier Transform;124
1.10.5;7.5 Fourier Analysis Demonstration;124
1.10.6;7.6 Conclusion and Future Work;128
1.10.7;References;128
1.11;Chapter 8 Modeling Time-Triggered Architecture Based Real-Time Systems Using SystemC;131
1.11.1;8.1 Introduction;131
1.11.2;8.2 Related Work;133
1.11.3;8.3 Background;133
1.11.3.1;8.3.1 SystemC;133
1.11.3.2;8.3.2 Time Model;134
1.11.3.3;8.3.3 Component;134
1.11.4;8.4 Executable Time-Triggered Model (E-TTM);135
1.11.4.1;8.4.1 Elements and Relationships;135
1.11.4.2;8.4.2 Time;137
1.11.4.3;8.4.3 Execution;137
1.11.4.4;8.4.4 Communication;138
1.11.4.5;8.4.5 Model Assumptions;139
1.11.5;8.5 Real-Time Control-System Example;139
1.11.5.1;8.5.1 System Description;140
1.11.5.2;8.5.2 System Design;140
1.11.5.3;8.5.3 Simulation Results;142
1.11.6;8.6 Dependability Assesment Example;143
1.11.6.1;8.6.1 Design;144
1.11.6.2;8.6.2 Simulated Fault Injection (SFI);147
1.11.7;8.7 Conclusion;148
1.11.8;References;148
1.12;Chapter 9 Towards the Development of a Set of Transaction Level Models A Feature-Oriented Approach;150
1.12.1;9.1 Introduction;150
1.12.2;9.2 Feature-Oriented Programming;151
1.12.3;9.3 Feature-Oriented TPL Development;153
1.12.3.1;9.3.1 The Universality of TPL;153
1.12.3.2;9.3.2 Poor Support of OOP for TPL Development;153
1.12.3.3;9.3.3 FOP Support for TPL Development;156
1.12.3.3.1;9.3.3.1 First Point;156
1.12.3.3.2;9.3.3.2 Second Point;157
1.12.3.3.3;9.3.3.3 Third Point;157
1.12.3.4;9.3.4 Feature-Oriented TPL Development Method;158
1.12.4;9.4 Case Study: A Simple SoC;158
1.12.4.1;9.4.1 Domain Analysis;159
1.12.4.2;9.4.2 Domain Design;159
1.12.4.2.1;9.4.2.1 UT Feature;159
1.12.4.2.2;9.4.2.2 Timing Feature;160
1.12.4.2.3;9.4.2.3 Intr Feature;162
1.12.4.2.4;9.4.2.4 PowerEstimation Feature;162
1.12.4.3;9.4.3 Domain Implementation, Configuration and Generation;162
1.12.5;9.5 Conclusion;163
1.12.6;References;163
1.13;Chapter 10 Rapid Prototyping of Complex HW/SW Systems using a Timing and Power Aware ESL Framework;164
1.13.1;10.1 Introduction;165
1.13.2;10.2 Requirements and Existing Tools;165
1.13.2.1;10.2.1 Executable Specification;166
1.13.2.2;10.2.2 Estimation and Representation of Non-Functional Properties;167
1.13.2.3;10.2.3 System Simulation Including Non-Functional Properties;168
1.13.2.4;10.2.4 Integrated Framework;169
1.13.3;10.3 Proposed Concept;170
1.13.3.1;10.3.1 Executable Specification;171
1.13.3.1.1;10.3.1.1 Parallel Application Description;171
1.13.3.1.2;10.3.1.2 System Input Stimuli;172
1.13.3.1.3;10.3.1.3 User Constrained HW/SW Separation and Mapping;172
1.13.3.1.4;10.3.1.4 Architecture/Platform Description;172
1.13.3.2;10.3.2 Estimation and Model Generation;173
1.13.3.2.1;10.3.2.1 Hardware/Software Task Separation;173
1.13.3.2.2;10.3.2.2 Hard- and Software Estimation;173
1.13.3.2.3;10.3.2.3 Pre-existing IP and Virtual Component Models;175
1.13.3.2.4;10.3.2.4 Virtual System Generation;176
1.13.3.3;10.3.3 Virtual System Simulation;176
1.13.4;10.4 Conclusion;179
1.13.5;References;179
1.14;Chapter 11 Towards Accurate Source-Level Annotation of Low-Level Properties Obtained from Optimized Binary Code;181
1.14.1;11.1 Introduction;181
1.14.2;11.2 Timing Analysis of Embedded Systems;183
1.14.2.1;11.2.1 Simulation;183
1.14.2.2;11.2.2 Static Analysis;185
1.14.3;11.3 Source-Level Annotation;186
1.14.4;11.4 Reconstruction of Line Information from Binary Code;187
1.14.5;11.5 Implementation and Results;190
1.14.6;11.6 Further Work;194
1.14.7;11.7 Conclusion;194
1.14.8;References;194
1.15;Chapter 12 Architecture Specifications in CaSH;197
1.15.1;12.1 Introduction;197
1.15.2;12.2 Preliminary Remarks;199
1.15.2.1;12.2.1 Hardware Types;199
1.15.2.2;12.2.2 User Defined Types;200
1.15.2.3;12.2.3 Operations and Functions;200
1.15.2.4;12.2.4 Compilation Pipeline;200
1.15.3;12.3 Examples;201
1.15.3.1;12.3.1 Multiply-Accumulate;201
1.15.3.2;12.3.2 Remarks;202
1.15.3.3;12.3.3 Variants of a Fir-filter;202
1.15.3.4;12.3.4 Variant 1;202
1.15.3.5;12.3.5 Variant 2;204
1.15.3.6;12.3.6 Variant 3;204
1.15.3.7;12.3.7 Remarks;205
1.15.3.8;12.3.8 Higher Order Cpu;206
1.15.3.9;12.3.9 Remarks;208
1.15.3.10;12.3.10 Floating Point Reduction Circuit;208
1.15.3.11;12.3.11 Remarks;211
1.15.4;12.4 Conclusions and Future Research;211
1.15.5;Reference;211
1.16;Chapter 13 SyReC: A Programming Language for Synthesisof Reversible Circuits;213
1.16.1;13.1 Introduction;213
1.16.2;13.2 Reversible Logic;215
1.16.3;13.3 The SyReC Language;217
1.16.3.1;13.3.1 The Software Language Janus;217
1.16.3.2;13.3.2 The Hardware Language SyReC;218
1.16.4;13.4 Synthesis of Circuits;219
1.16.4.1;13.4.1 Reversible Assignment Operations;220
1.16.4.2;13.4.2 Binary Operations;221
1.16.4.3;13.4.3 Conditional Statements, Loops, Call/Uncall;222
1.16.5;13.5 Experiments;224
1.16.6;13.6 Conclusions and Future Work;226
1.16.7;References;226
1.17;Chapter 14 Logical Time @ Work: Capturing Data Dependencies and Platform Constraints;229
1.17.1;14.1 Introduction;229
1.17.2;14.2 Background;231
1.17.2.1;14.2.1 ccsl in a Nutshell;231
1.17.2.2;14.2.2 Process Networks Semantics;233
1.17.3;14.3 Synchronous Data-Flow;234
1.17.3.1;14.3.1 Semantics Based on Data Dependency;234
1.17.3.2;14.3.2 Semantics Based on Execution Dependency;235
1.17.3.2.1;14.3.2.1 Encoding the Local Scheduling in ccsl;235
1.17.3.2.2;14.3.2.2 Local Scheduling Algorithm;237
1.17.3.3;14.3.3 Semantics Comparison;238
1.17.4;14.4 Extensions to Multidimensional Data-Flow;239
1.17.4.1;14.4.1 Semantics;239
1.17.4.2;14.4.2 Encoding MDSDF in ccsl;239
1.17.5;14.5 External Constraints;241
1.17.6;14.6 Discussion and Conclusion;243
1.17.7;References;243
1.18;Chapter 15 Formal Support for Untimed MARTE-SystemC Interoperability;245
1.18.1;15.1 Introduction;246
1.18.2;15.2 Related Work;248
1.18.2.1;15.2.1 ForSyDe;249
1.18.3;15.3 MARTE Specification Methodology;250
1.18.4;15.4 SystemC Model;253
1.18.5;15.5 Formal link Between MARTE and SystemC;255
1.18.6;15.6 Formal Support for Untimed SystemC Models;257
1.18.7;15.7 Conclusions;258
1.18.8;References;258