Transcript
See discussions, stats, and author profiles for this publication at: https://www.researchgate.net/publication/220689081 Compiling Esterel. Book · January 2007 DOI: 10.1007/978-0-387-70628-3 · Source: DBLP CITATIONS 31 READS 62 3 authors: Dumitru Potop-ButucaruNational Institute for Research in Computer S… 39 PUBLICATIONS 446 CITATIONS SEE PROFILE Stephen A. EdwardsColumbia University 144 PUBLICATIONS 3,518 CITATIONS SEE PROFILE Gérard BerryCollège de France 166 PUBLICATIONS 10,347 CITATIONS SEE PROFILE All content following this page was uploaded by Dumitru Potop-Butucaru on 15 December 2016. The user has requested enhancement of the downloaded file. Compiling Esterei Dumitru Potop-Butucaru Stephen A. Edwards Gerard Berry Springer Contents Preface vii I The Esterei Language 1 Introduction to Esterei 3 1.1 Reactive Systems 3 1.2 The Synchronous Hypothesis 4 1.3 Implementation Issues 5 1.4 Causality 6 1.5 Related work 6 1.6 A First Esterei Example 7 1.7 Causality Cycles 8 1.8 Code Generation 9 1.8.1 Translation to Explicit State Machines 9 1.8.2 Translation to Circuits 10 1.8.3 Direct Compilation to C Code 12 1.9 Executing the Generated Code 12 1.9.1 Existing Solutions 13 2 The Esterei Language 15 2.1 Syntax and Naive Semantic Principles 15 2.2 The Kernel Esterei Language 20 2.3 Esterei Through Examples 24 2.4 Host Language 31 2.5 Program Structure and Interface 31 2.5.1 DataHandling 32 2.5.2 Signal and Signal Relation Declarations 34 2.5.3 The run Pseudo-Statement 34 XI Xll CONTENTS II Formal Semantics 3 Introduction to Esterei Semantics 41 3.1 Intuition and Mathematical Foundations 41 3.1.1 The Constructive Approach 43 3.2 Flavors of Constructive Semantics 47 3.3 Conventions and Preliminary Definitions 50 3.3.1 Global Correctness of an Esterei Program 50 3.3.2 Restriction to Kernel Esterei 51 3.3.3 Signal Events 51 3.3.4 Trap Handling and Completion Codes 51 4 Constructive Behavioral Semantics 55 4.1 Behavioral Transitions 55 4.1.1 Transition syntax 55 4.1.2 States as Decorated Terms 56 4.1.3 State Syntax 57 4.2 Analysis of Potentials 58 4.2.1 The Definition of Must, Can, and Can 60 4.2.2 Elementary Properties 68 4.3 Semantic Rules 68 4.4 Proof 72 4.5 Determinism 72 4.6 Loop-Safe Programs. Completion Code Potentials 73 4.7 Program Behavior 75 5 Constructive Operational Semantics 79 5.1 Microsteps 80 5.2 COS Terms 80 5.2.1 Control Flow Propagation 81 5.2.2 State-Dependent Behavior 81 5.2.3 Syntax of Semantic Terms 82 5.3 Data Representation 84 5.4 Semantic Rules 85 5.4.1 Rules for Pure Esterei Primitives 85 5.4.2 Rules for Data-Handling Primitives 92 5.5 Analysis of Potentials 95 5.5.1 Reduction to Non-Dotted Terms 96 5.5.2 Non-Dotted Terms over Dataless Primitives 97 5.5.3 Non-Dotted Terms over Data-Handling Primitives . . 99 5.6 Behaviors as Sequences of Microsteps 99 5.7 COS versus CBS 101 CONTENTS x 6 Constructive Circuit Translation 103 6.1 Digital Circuits with Data - 104 6.1.1 Circuit Semantics. Constructive Causality 104 6.1.2 Extension to Circuits with Data 107 6.1.3 Formal Definitions 110 6.2 Translation Principles 112 6.2.1 The Selection Circuit 114 6.2.2 The Surface and Depth Circuits 115 6.2.3 The Global Context 116 6.3 Translation Rules 117 6.3.1 Dataless Primitives 117 6.3.2 Data-Handling Primitives 126 6.4 Circuit Translation versus COS 128 III Compiling Esterei 7 Overview 135 7.1 Compiler Classes 135 7.2 A Brief History 136 7.3 The INRIA Compiler 137 7.4 The Synopsys Compiler 139 7.5 The Saxo-RT Compiler 140 7.6 The Columbia Esterei Compiler 144 8 The GRC Intermediate Format 145 8.1 Definition and Intuitive Semantics 146 8.1.1 The Hierarchical State Representation 146 8.1.2 The Control/Data Flowgraph 149 8.1.3 Implementation Issues 154 8.2 Esterei to GRC Translation 158 8.2.1 Translation Principles 158 8.2.2 Translation Rules 159 8.2.3 The Global Context 167 8.3 Formal Simulation Semantics and Translation Correctness . 167 8.4 Format Optimizations 168 8.4.1 State Representation Analysis 170 8.4.2 Flowgraph Optimizations 173 9 Code Generation from GRC 179 9.1 Defining Acyclic 180 9.2 Code Generation for Acyclic Specifications 185 9.2.1 State Encoding 185 9.2.2 Flowgraph Transformations 190 9.2.3 Scheduling 192
