Titre : Sémantique Formelle d'une Infrastructure de Compilation

Keywords: Formal Semantics of Hardware Compilation Framework Modeling of processor design, Hardware Construction Languages (HCLs), Pipeline datapath, Timing anomalies, Model checking

Matériel

Mots clés : Modélisation des processeurs, Langages de Construction de Matériel (HCLs), Chemin de données du pipeline, Anomalies temporelles, Vérification de modèle Résumé : Les analyses statiques de pire temps d'exécution sont utilisées pour garantir les délais requis pour les systèmes critiques. Afin d'estimer des bornes précises sur ces temps d'exécution, ces analyses temporelles nécessitent des considérations sur la (micro)architecture. Habituellement, ces modèles de micro-architecture sont construits à la main à partir des manuels des processeurs. Cependant, les initiatives du matériel libre et les langages de description de matériel de haut niveau (HCLs), permettent de réaborder la problématique de la génération automatique de ces modèles de micro-architecture, et plus spécifiquement des modèles de pipeline. Nous proposons un workflow qui vise à construire automatiquement des modèles de chemin de données de pipeline à partir de conceptions de processeurs décrites dans des langages de contruction de matériel (HCLs). Notre workflow est basé sur la chaine de compilation matériel Chisel/FIRRTL. Nous construisons au niveau de la représentation intermédiaire les modèles de pipeline du chemin de données. Notre travail vise à appliquer ces modèles pour prouver des propriétés liées à la prédictibilité temporelle. Notre méthode repose sur la vérification formelle. Les modèles générés sont ensuite traduits en modèles formels et intégrés dans une procédure existante basée sur la vérification de modèles pour détecter les anomalies de temps. Nous utilisons le langage de modélisation et de vérification TLA+ et expérimentons notre analyse avec plusieurs processeurs RISC-V open-source. Enfin, nous faisons progresser les études en évaluant l'impact de la génération automatique à l'aide d'une série de critères synthétiques.

Dedications

I dedicate this humble work with great love and pride To my dearest mother Khadija EL GAREH

To my dearest mother, may you find here the homage of my gratitude, which will be equal to your sacrifices and prayers for me, however great it may be. You represent the source of tenderness and the example of devotion that never ceased to encourage and pray for me. No dedication is eloquent enough to express what you deserve for all the sacrifices you have constantly made during my childhood and even adulthood. I dedicate this work to you as a token of my deep love. May God, the Almighty, preserve you and grant you health, long life, and happiness.

To my dear father Mohammad AIT BENSAID

To the good Lord and you, the man in my life, for being able to live this day. The world could compensate for all the sacrifices you made for my education and well-being so that I could devote myself to my studies. A thousand thanks for all your sacrifices, your Alas, no dedication can express my love for you. May Almighty God preserve you and grant you health, long life, and happiness.

To my brothers Noureddine, Youssef, and Zakaria

For their love and undeniable support. Words cannot express my attachment, love, and affection for you. I wish you a future full of joy, happiness, and success.

To my friends, for the moments we've shared and for your support.

To my supervisors and everyone who has helped me, I dedicate this work to them in recognition of their invaluable support. 9

Acknowledgment

This experience spent within CEA List and the Paris-Saclay University would never have been so fruitful without the contribution of some people I would like to thank.

I am particularly grateful to my three supervisors, Mathieu Jan, Mihail Asavoae, and Farhat Thabet, for their continuous support of my research. They ensured this project's progress and provided rigorous and professional seriousness in a friendly, relaxed climate with disconcerting virtuosity. I am very grateful for their wise advice, immense knowledge, and guidance.

I would like to thank my jury members, Dr. Stephan Merz, Prof. Steven Derrien, Prof. Jean-Luc Bechennec, Prof. Isabelle Puaut, and Prof. Laurent Pautet, for having accepted to evaluate my work and for their perceptive comments.

I also thank all my labmates; it has been great sharing the laboratory with you during these past three years.

Finally, I thank my family and friends who supported me with moral and emotional support during my thesis years. 11

-Introduction

Embedded systems are designed with specific functionalities in mind and integrated into more complex systems. Embedded systems have a hardware infrastructure (e.g., processor-based) and are capable of executing applications that address those specific functionalities. These systems are used in various application contexts, ranging from portable devices such as phones to safety-critical medical, aerospace, and transport systems. Safety-critical systems induce computing constraints, which depend on several factors. More specifically, we consider safety-critical systems as real-time embedded systems whose correctness depends not only upon their functional correctness but also upon the time in which they are performed.

The design and implementation of safety-critical systems rely on regulations and standards that state functional and non-functional constraints to be satisfied. Functional requirements are essential so that the system can operate correctly. However, these systems are also subjected to non-functional aspects such as hard real-time requirements, and their design is standardized to help identify and address potential hazardous events [START_REF] Kaestner | Safety standards and wcet analysis tools[END_REF]. For example, events like missing timing deadlines would be deemed unacceptable since respecting these deadlines is mandatory for safety-critical systems. Specialized timing analyses (i.e., worst-case) are required to derive adequate timing bounds and to characterize, in this way, the timing behavior of a system under consideration. The timing properties must be handled at different steps of the design process. Thus, the hardware designers have started to integrate these properties in the early design stages, from modeling to execution. The failure to meet deadlines and the timing vulnerabilities may be as harmful as producing inaccurate outputs or causing system damage. We characterize the timing behavior of these systems with adequate timing bounds (worst-case execution time considerations) [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF] [START_REF] Lothar | Design for Timing Predictability -Real-Time Systems[END_REF].

Static worst-case timing analysis [START_REF] Ballabriga | OTAWA: an open toolbox for adaptive WCET analysis[END_REF][START_REF] Hardy | The heptane static worst-case execution time estimation tool[END_REF][START_REF] Li | Chronos: A timing analyzer for embedded software[END_REF] is one of the approaches used to estimate these deadlines and can compute safe and precise bounds on the timing behavior of the system. Such analyses consider the executions of an input program on an underlying architecture in order to account for accurate results. In this setting, both aspects of the program and the architecture considerations become equally important. Whereas the program-level infrastructure required by the WCET analysis relies on the control-flow graph (i.e., the input program is the binary), at the architecture level, the WCET analysis infrastructure is more diverse. For example, the same control-flow graph is used for cache analyses [START_REF] Lv | A survey on static cache analysis for real-time systems[END_REF] whereas more specialized, cycle-accurate models are necessary for pipeline analyses [START_REF] Engblom | Processor pipelines and their properties for static WCET analysis[END_REF].

Thus, the need to model the design architecture is paramount to verify the required timing constraints. Several static timing analyzers exist, for example, the industrial-strength tool aiT [START_REF] Langenbach | Pipeline modeling for timing analysis[END_REF] and the academic WCET analyzers Otawa [START_REF] Ballabriga | OTAWA: an open toolbox for adaptive WCET analysis[END_REF], Heptane [START_REF] Hardy | The heptane static worst-case execution time estimation tool[END_REF] and Chronos [START_REF] Li | Chronos: A timing analyzer for embedded software[END_REF]. All these propose handcrafted models of (micro)-architecture (i.e., caches and pipelines), relying on static analysis to characterize their timing behaviors, and validated against hardware simulators for conformance (e.g., for aiT [START_REF] Wilhelm | Testing implementation soundness of a WCET analysis tool[END_REF] or Chronos [START_REF] Burger | The simplescalar tool set, version 2.0[END_REF]). A closer code inspection of their pipeline models exposes their common attributes. First, these pipelines present a "flat" structure. More precisely, the pipeline stages are represented with simple state configurations (i.e., a single variable), reducing a pipeline stage to an identification attribute. The pipeline components are separated into smaller units with inner states. This separation reduced the complexity and made the implementation easier. Second, these models focus on how an instruction progresses through the pipeline, not the actual instruction semantics. Indeed, the correctness of program execution is assumed in the context of static WCET analysis, and the worst-case upper bounds are defined through the execution of the input program on the pipeline model. Furthermore, various models are built from low-level hardware designs such as VHDL and Verilog [3].

However, the manufacture and production of these hardware designs are evaluated according to several criteria, and the design time is one of the primary criteria. Furthermore, the low-level hardware description languages describe in more detail the designs and reduce the production speed in exchange. Since their micro-architecture models are usually huge, generating pipeline analysis that covers the timing behavior of the design would increase the state space, making the WCET determination a challenging task. Thus, we need to opt for high-level abstraction languages and generate these timing models automatically. With an automatic procedure, we speed up the process and reduce the model's size by pruning out all parts that do not contribute to the timing behavior. Moreover, we avoid losing information, and we guarantee that the timing analysis of the design is feasible with a precise computation of upper bounds. So, developing such models at a proper abstraction level is essential to obtain correct and precise WCET bounds.

Automatically deriving architecture models [3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] directly from the code of hardware designs can also be possible. Unsurprisingly, the accuracy of the resulting architecture models depends on how the hardware design is coded. For example, in the case of a pipeline design, a modular code with a clear separation between datapath and control facilitates the construction of the architecture model. Recent trends in hardware design led to more processor code being made available, i.e., open-source. Thus, it can be used to generate models, replacing the standard manual reference, where only specific design details are provided. This progress is facilitated by the emergence of open hardware initiatives [START_REF] Asanović | Instruction sets should be free: The case for risc-v[END_REF]. Such initiatives propose software-like development workflows, from complex high-level Hardware Description Languages (HDLs) [START_REF] Bachrach | Chisel: constructing hardware in a scala embedded language[END_REF] down to circuits while using sophisticated compilation chains.

High-level hardware description languages (e.g., Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF] or SpinalHDL [START_REF] Papon | SpinalHDL[END_REF]) provide new features to hardware designers while, at the same time, speeding up development by being able to generate fast simulations of the design. While low-level, mainstream languages like VHDL and Verilog are still almost ubiquitous in the industry, their age and original intention put them behind current high-level languages regarding productivity and flexibility. High-level design languages come with their associated compilation framework, enabling the use of highly parameterized generators and advanced module systems to facilitate the hardware design [START_REF] Bachrach | Chisel: constructing hardware in a scala embedded language[END_REF] [21] [START_REF] Papon | SpinalHDL[END_REF]. These compilation chains come with configurable optimizations and a pass infrastructure, which facilitate the analysis of hardware designs. For instance, when targeting timing predictability, a transformation would mainly focus on the sequential logic to generate pipeline-level models. The main goal of our thesis work is to automatically generate pipeline models from high-level hardware processor designs so as to prove timing properties.

To prove these requirements of safety-critical systems, various methods can be used, from testing to formal verification, offering different degrees of confidence. Testing is a standard method used for validation, but it is not exhaustive. Formal verification is another method used for validation; it could be exhaustive but requires building formal models. We adopt formal verification as our approach, with the goal of generating formal micro-architecture models as pipeline models from open-source processor designs. Then, we can formally verify the properties related to timing predictability, such as the detection of timing anomalies [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF].

. Scientific Contributions

Considering the context and the main motivations presented in the previous section, our proposed work leads us to define two main goals to get around the above-mentioned motivations. The first goal is the automatic generation of pipeline models. The second goal is to integrate these pipeline models into a formal framework for the verification of timing properties, for example, the detection of timing anomalies. As a result, we summarize these goals in four main contributions.

As a first contribution, we propose a general workflow to achieve our goals. The workflow targets the automatic generation of pipeline models for the formal verification of timing properties. We specify each component with a highlight of the hardware compilation framework as the first brick of the workflow.

The second contribution concerns the register analysis and the construction of data structure representation of the abstract datapath pipeline models. In this context, we rely on the high-level hardware processor designs de-veloped with Chisel language [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF] and its associated compilation framework Chisel/FIRRTL [START_REF] Izraelevitz | Reusability is firrtl ground: Hardware construction languages, compiler frameworks, and transformations[END_REF] that provides the possibility to integrate passes. Thus, the problem of deriving convenient datapath pipeline models is backed by a comprehensive hardware compilation infrastructure. The approach proposed to derive register analysis is applied to various processor designs.

The third contribution concerns the pipeline datapath construction based on the results of the register analysis. In this phase, the registers are assigned to pipeline stages through several algorithms. The aim is to build the abstract datapath models as a succession of pipeline registers assigned in their identified pipeline stages. We report our proposed approach and evaluate its effectiveness in several case studies as Chisel-based RISC-V processors.

Finally, the last contribution intends to generate automatically the required formal models to prove formally the timing predictability properties and then to integrate them into a procedure for the detection of timing anomalies. We automatically generate the formal datapath pipeline models. Then we manually specify the control signals to guide the pipeline execution. In this direction, we combine both the software (ISA representation) with the hardware (pipeline models) aspects. Therefore, we formally verify the absence/presence of timing anomalies on the resulting models with the procedure presented in [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF]. The objective is to evaluate the impact of semi-automatically generated models through a series of synthetic benchmarks.

. Outline

The remainder of this manuscript is organized as follows:

• Chapter 2: We present the background of our work, including the hardware construction languages, the RISC-V processor designs used to evaluate our work and the formal verification framework. We also highlight our chosen hardware language and its compilation framework. • Chapter 3: We review state of the art works that build the microarchitecture models from hardware designs. We detail each axis of our contributions. We introduce then the problem statement of our work. • Chapter 4: We introduce our general workflow that aims to verify timing properties on hardware designs, formally. • Chapter 5: We describe in this chapter the register analysis as well as its evaluation. • Chapter 6: We describe the pipeline construction algorithm through an assignment of registers to pipeline stages. We report the application and the experimental results of several processor designs. • Chapter 7: We present the generation of formal models followed by the integration of these formal models into the procedure to detect timing anomalies. We rely on several benchmarks to evaluate our results. • Chapter 8: We describe conclusions and some perspectives of our work.

-Background

In this chapter, we introduce the background concepts on which this thesis work is based. In Section 2.1, we present a general background on hardware construction languages (HCLs) and their compiler frameworks, then elaborate on our chosen hardware language Chisel, and its compilation framework Chisel/FIRRTL. In Section 2.2, we continue with an overview of the processor designs considered as case studies in this work. Then, Section 2.3 introduces notions related to formal verification methods and tools.

All these elements introduced in this chapter allow us to emphasize the problems addressed in the next chapters precisely.

. Hardware Construction Languages and their Compilation

Overview of HCLs. When we discuss about hardware designs, there is a need to find a method to ease communication and understand the functionality of each design component. As such, the hardware designs are developed with hardware description languages (HDLs) to present the structure and functionality at different abstraction levels. When hardware designers intended to increase design productivity and efficiency with shorter design cycles, they relied on hardware generators and design reuse in particular libraries reuse, as in software programming. Thus, hardware designers use high-level languages called hardware construction languages (HCLs), which embed HDL-like hardware primitives in existing programming languages.

These languages enable the use of software programming features such as object orientation, polymorphism, and higher-order functions, which encourage and enable code reuse. Furthermore, these expressive language features make designs more parameterizable and modular and enable the use of domain-specific language constructs, and advanced module systems to facilitate the hardware design [START_REF] Bachrach | Chisel: constructing hardware in a scala embedded language[END_REF][START_REF] Papon | SpinalHDL[END_REF][START_REF] Schuiki | LLHD: a multi-level intermediate representation for hardware description languages[END_REF]. These languages are supported by hardware compiler frameworks (HCFs) which can put hardware development on an important evolution by enabling new hardware libraries. Furthermore, HCFs transform a high-level purpose code into an RTL level by formalizing various transformations. These transformation passes enable the reuse and optimization of the HDL (Verilog or VHDL) code they generate for later use as input in classical commercial (FPGA or ASIC) hardware design flows. As in software compilers, hardware designers can also insert specific transformation passes in those compilation chains to manipulate the designs. This feature enables to deploy, within these chains, analyses to construct abstract processor models automatically. For instance, when targeting timing predictability, a transformation would mainly focus on the sequential logic to generate pipeline-level models.

Several hardware construction languages are introduced and developed for hardware designs. Usually, they are based on software programming languages such as C++, Python, and Scala. Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF], BlueSpec [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF], Spinal-HDL [START_REF] Papon | SpinalHDL[END_REF], and DFiant [START_REF] Port | Dfiant: A dataflow hardware description language[END_REF] are the most modern hardware construction languages that can be seen as domain-specific languages, where they leverage host language ideas and software engineering techniques. We focus in our work on an HCL called Chisel, supported by the compilation framework Chisel/FIRRTL.

Chisel/FIRRTL Hardware Compiler Framework. Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF] is a hardware construction language (HCL) developed at UC Berkeley, embedded in the Scala language and thus, implemented as a package of Scala class libraries. Chisel provides powerful constructs for writing hardware generators. We take, as examples, parameterization and higher-order functions.

Table 2.1 summarizes the primary Chisel constructs, specifying their syntax and semantics. We distinguish between basic elements such as types, operators, etc. state elements corresponding to registers and memory components, and finally high-level constructs such as interfaces. Chisel provides three data types: Bits, UInt, and SInt. All three types represent vectors of bits. Here is the definition of different such types: a plain 6-bit, an 6bit unsigned integer, and a 10-bit signed integer, with W specifying the width: Bits(6.W), UInt(6.W), SInt(10.W).

Interfaces are presented in Chisel by DecoupledIO and ValidIO language constructs. Chisel defines the DecoupledIO bundle in the following way: bits is used for the data and is parameterized with the data type. ValidIO is similar to DecoupledIO except that it only has valid and bits fields. We detail other constructs with particular processor designs in Section 4.2. The Listing 2.2 illustrates the parameterization features of the Chisel language. Chisel uses parameterized types to specify generic functions and classes.

The function Mux, line 11 in Listing 2.2 describes the parameterized function and semantically it defines a generic multiplexer function. We define this function as taking a boolean condition, con, and alt arguments (corresponding to x := y Assign wire y to x

x <> y Bulk connect x and y

Interfaces

DecoupledIO(gen: Data) gen: Chisel Data to wrap with a ready valid interface.

Interface: (in) .ready: ready Bool (out) .valid: valid Bool (out) .bits: data

ValidIO(gen: Data)

Wrap gen with a valid interface.

Interface: (out) .valid: valid Bool (out) .bits: data then and else expressions) of type T which is required to be a subclass of Bits. The assignment to mux1, in line 15, specifies the parameter values.

Like parameterized functions, we can also parameterize classes to make them more reusable. For instance, we can generalize the Adder class, lines 3-12 in Listing 2.2 to add any type T which is a generic type defined in the package chisel3.Data. We define two instances of this class add1 and add2, lines 13-14, to take two arguments genIn and, genOut of type T.

Listing 2.2 -Parameterization in Chisel, inspired from [START_REF]chisel-bootcamp[END_REF]. def Mux[T <: Bits](c: Bool, con: T, alt: T): T = { ... } 12 } 13 val add1 = new Adder(UInt(4.W), UInt(6.W)) 14 val add2 = new Adder(SInt(4.W), SInt(6.W)) 15 val mux1 = add1.Mux(true.B, UInt [START_REF] Hardy | The heptane static worst-case execution time estimation tool[END_REF], UInt(11)) 16 ... Listing 2.3 describes high-order functions in Chisel that take functions as arguments. These are powerful constructs that encapsulate a general calculation model, allowing one to concentrate on the application logic instead of the control flow. These functions include the map and reduce functions. Function map, line 2 in Listing 2.3, invokes a function (successor) on each element of the list and returns a list of the function's return value. Function reduce, line 3 in Listing 2.3, takes two arguments: the first is the current accumulation and the second represents the list element. These are given by the two underscores in the parentheses. It returns a value with a type of the list elements, unlike map, which returns a list.

Listing 2.3 -Higher-order functions in Chisel.

1 ...

List (1,2,3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF].map(_ + 1) /* return List(2,3,4,5) */ List (1,2,3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF].reduce(_ + _) /* return 10 */ ...

.1 illustrates the Chisel/FIRRTL hardware compiler framework. Once a Chisel design is compiled, a Verilog file is generated via an intermediate representation FIRRTL [START_REF] Izraelevitz | Reusability is firrtl ground: Hardware construction languages, compiler frameworks, and transformations[END_REF], which can then be processed with any standard RTL design flow.

An important part of any compiler is its intermediate representation (IR), upon which all transformations operate. FIRRTL transformations always take as input and produce a well-defined AST circuit and are easily connected one after the other. These transformation passes provide simplification, optimization, analysis, specialization, and instrumentation and the resulting representation can either be simulated directly or passed to one of many Verilog back- Afterward, transformations go through two simplifications, from high form to mid-form and from mid-form to low form. In the mid-form, the conditional statements (when) are not used; thus, the pass ExpandWhensAndCheck addresses this point. Also, all widths must be explicitly defined, and fields in connections must be detailed using the ExpandConnects pass. The low form gives a direct correspondence to a circuit netlist. For instance, the partial connect statements are not used in this form, thus the pass LegalizeConnects is used. Moreover, the synchronous Reset is removed with the RemoveReset pass. Finally, the low form is directly compiled into Verilog. Therefore, various passes are implemented to make changes to the FIRRTL AST to make Verilog emission easier. We mention the FlattenRegUpdate pass, which flattens register updates into a single expression, and VerilogPrep pass, which adds wires to connect port interfaces between instances.

Furthermore, writing a transformation saves effort for all future uses, reducing the cost of the development over time. By making transformations easy to write and integrate into a compiler framework, the upfront development cost of a transformation is reduced, and the number of interesting automatable tasks increases. Writing a FIRRTL pass usually requires writing functions that walk the FIRRTL data structure. The intermediate representation (IR) of FIRRTL is a tree, where each IR node can have the children nodes. The recursive walk collects information or replaces IR nodes with new IR nodes.

Next, in Listing 2.4, we present an example of the transformation that expresses a recursive walk to collect the names of every register declared in the design. We apply a custom map function for each node and then to the subset of children whose node type matches the function's input and return node type, line 7 in Listing 2.4. When the node is a register, we collect its name into a list structure.

. Pipelined Processors

We present next the various pipelined hardware designs evaluated and used as case studies in this work. We start with an overview of the pipeline features that are considered in the hardware designs and which impact our analysis, in Section 2.2.1. Then, we present the primary use case studies of hardware designs, in Section 2.2.2.

. Pipelining Concepts

Pipelining is a process of arrangement of hardware elements of the processor such that its overall performance is increased. The process of executing one instruction can be divided into several sequential sub-operations, with each sub-operation corresponding to a pipeline stage. The processor can execute instructions in the order that they appear in the program, as is the case of in-order pipelines. The pipeline stages for the classic in-order pipeline, shown in Figure 2 A pipeline consists of the datapath and control path. The datapath can be defined as the path that the instructions must fulfill within the processor to finish their execution. Different instructions may need different datapaths and an instruction generally requires more execution time to fulfill a longer path within the datapath. The control path ensures the correct transmission of data and controls the execution status of the instructions at each pipeline stage. The control path defines the pipeline status by identifying stalling and forwarding mechanisms and establishes signals for instructions decoding.

Figure 2.3 shows the stages of a standard in-order 5-stage pipeline, i.e., from the Instruction Fetch (IF) stage to the register Write-Back (WB) stage. The pipeline control, represented with dotted lines, captures how instructions advance (i.e., the next PC value) through the pipeline. The stalling logic is, however, not explicitly represented, but it can be inserted in any pipeline stage. The datapath, presented with solid lines, considers the usual left-to-right advancement through the pipeline stages, with optimization in the form of register forwarding, represented with blue lines. The forwarding mechanism depends on the architecture and in which stage an instruction requires/produces the dependencies. The processors employed in our work and whose pipelines strictly adhere to this representation are shown in Fig. 2.3.

The pipeline execution of the processors divides the execution of instructions into several steps without affecting the performance. In contrast, the step duration can be reduced by increasing the number of steps and therefore, reducing the processor's cycle time. However, there are various cases where pipeline performance is degraded, called pipeline hazards. Hazards are pipelined execution problems caused when an instruction is unable to be executed in its designated cycles. There are three types of hazards: data, control, and structural hazards.

Structural hazards result from sharing resources between instructions. They occur when more than one instruction needs to use the same datapath resource simultaneously. There are two main causes of structural hazards:

• Register File: The simultaneous access to the register file leads to structural hazards. The register file is accessed both during ID when it is read and during WB when it is written. We can solve this by having separate read and write ports. To account for reads and writes to the same register, processors usually write to the register during the first half of the clock cycle and read from it during the second half. This is also known as double pumping. • Memory: Memory is accessed for both instructions and data. The IF and MEM stages both transfer data over the memory bus. Having a separate instruction memory and data memory solves this hazard. Structural hazards can always be resolved by adding more hardware. Control hazards could occur when instructions of type jump and branch are in execution. If a dynamic branch instruction occurs, either as a conditional branch or an indirect jump, the fetch stage (PC) cannot continue to fetch the next instruction (next sequential PC) after the branch, but the computation result of the argument to the branch completed in the EX stage. Thus, we should stall the pipeline for control hazards, but this decreases performance.

Branch prediction attempts to resolve a branch hazard by predicting which path to take.

Data hazards are due to data dependencies between instructions: an instruction requires an unavailable result of the previous instruction. Existing solutions to handle data hazards include forwarding mechanisms [START_REF] Bernardi | On the functional test of the register forwarding and pipeline interlocking unit in pipelined processors[END_REF], code reordering and pipeline stalling. There are three situations in which a data hazard can occur:

• Write After Read (WAR): An anti-dependency hazards occur if an instruction writes a register that is read by a previous instruction. Here it must be guaranteed that the write occurs only after the first instruction has read the register. This type of hazard cannot occur in in-order processors since instructions are always executed in the primary fixed order. • Write After Write (WAW): an output dependency, hazards occur if a subsequent instruction writes the same register as a previous one. It must be guaranteed that only the last write is performed to the register file. Again, for in-order pipelines with only a single write-back stage, this hazard cannot occur. • Read After Write (RAW): A true dependency hazards occur if a subsequent instruction reads a register that is written by a previous instruction. This dependency is resolved by the forwarding mechanism to avoid additional delays. Forwarding is an efficient method in solving the data dependencies between instructions, more precisely when a destination operand of an instruction is the source operand(s) of a subsequent instruction(s). Forwarding is implemented using combinational logic units (i.e., multiplexers and comparators) to test these dependencies. For instance, it uses multiplexers and structural conditions in order to test if there is a data dependence between the instruction's operands. Furthermore, the forwarding mechanism presents several possible paths. It depends on various criteria; the data dependence between instructions is the first. However, the addition of wires also depends on the architecture of the processors, in particular, the stage in which the instruction should be executed in order to produce/require the data.

A complete forwarding consists of several paths. The main possible cases include three paths. There are thus 3 forwarding paths illustrated in Figure 2.3 1 -3 , from the pipeline stages Execute (EX), Memory (MEM) and Write-Back (WB) to EX respectively.

. HDL Designs: RISC-V Processors Overview

RISC-V is a modern, open-source Instruction Set Architecture (ISA) that has gained significant momentum in recent years. Moreover, RISC-V is designed from the ground up to enable the integration of custom instruction set extensions in order to build highly application-specific solutions. Most Chisel-based processor designs are built to support RISC-V ISA. We present next several hardware processor designs used to evaluate our work. They are developed in the Chisel language and compiled with the Chisel/FIRRTL hardware compilation framework. These processors' pipeline structure ranges from 3 to 6 pipeline stages. We present RISC-V Sodor [1], RISC-V Mini [START_REF]Risc-v mini[END_REF], KyogenRV [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF], Rocket [2] and Fuxi [START_REF]Fuxi, a 32-bit pipelined risc-v processor written in chisel3[END_REF] processors.

RISC-V Mini. RISC-V Mini [START_REF]Risc-v mini[END_REF] proposes a simple three-stage pipeline designed to serve as an initial test case when designing the last versions of Chisel. RISC-V-mini is implemented using Chisel, hardware design language, version '3.5'. It has been a crucial example in various project developments, including the languages Chisel3 and FIRRTL as well as their respective simulation and verification methodologies. It implements RV32I of the Base Integer User-level ISA Version 2.0. It also consists of an instruction cache and a data cache.

RISC-V Sodor.

Sodor [1] is a family of processors coming with different pipeline depths. We consider its 3 and 5 stages versions in our work. It is an open-source RISC-V project for educational purposes as well as to enable a broad range of developers to learn and utilize RISC-V ISA quickly. It contains five 32-bit RISC-V CPUs to demonstrate simple RISC-V ISA written in Chisel. These CPUs are named from RV32-1-stage to RV32-5-stage. Furthermore, each core has its features. For example, the RV32-1-stage is used essentially as an ISA simulator, and the RV32-2-stage is mainly employed to demonstrate pipelining in Chisel. RV32-3-stage uses sequential memory, while RV32-5-stage can toggle between fully bypassed or fully interlocked. Figure 2.4 illustrates the RV32-5-stage of Sodor processor design. Its pipeline is a classic 5-stage pipeline where instructions pass through the following stages: IF (Instruction Fetch), ID (Instruction Decode), EX (Execute), MM (Memory), and WB (Write-Back). [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF] is also an open-source five-stage pipeline processor targeting Intel FPGAs and developed for academic purposes. It is written in Chisel version '3.5'. It implements RV32I of the User-level ISA Version 2.2.

KyogenRV. KyogenRV

Rocket.

Rocket is an in-order scalar processor originally developed at UC Berkeley, initially designed for ASICs but can be built for an FPGA and features OS support. The Rocket core is used as a component within the Rocket Chip SoC generator which is a Scala program that invokes the Chisel compiler in order to emit RTL describing a complete SoC. Rocket core is based on the RV64GC RISC-V Instruction Set Architecture (ISA) [START_REF] Waterman | The RISC-V instruction set[END_REF], and is written in Chisel language, version '3.5'. The Rocket core is a 5-stage pipeline, however, it is sometimes presented as a 6-stage pipeline with a separate stage pcgen, implementing the branch prediction. Rocket core contains L1 data and instruction caches, integer ALU and an optional floating-point unit (FPU). The Rocket core is written in Chisel language and arranged into modules (Core, Frontend, BTB, etc.). The first two stages, Pcgen, and Fetch, are implemented in the Frontend module, while the remaining four pipeline stages are contained within the core module.

Figure 2.6 describes the Fetch and Pcgen stages in detail. It includes a MMU that supports page-based virtual memory with a translation lookaside buffer (TLB), a non-blocking data cache, and a front-end with branch prediction which is provided by a branch target buffer (BTB), branch history table (BHT), and a return address stack (RAS). While Figure 2.7 presents the Decode, Execute, Memory, and Write-Back stages. The core includes the optional FPU, the configurable functional unit pipelines, and the privileged architecture implementation (i.e., the control and status register file). The connection between these two parts is described in more detail in Section 4.3.3. Fuxi. Fuxi is a 32-bit pipelined RISC-V processor designed for running simple operating systems or bare-metal software. Fuxi implements RV32I ISA and is implemented in Chisel language, version '3.2'.

. Formal Methods Overview

The process of modeling and verification of properties of hardware designs considers two main phases. The first phase focuses on creating an abstract model and validating the abstraction. The second concerns verifying the properties of the abstract model. System modeling is carried out taking into account the level of abstraction required for properties to verify. Various abstract models can exist depending on the type of targeted properties and the level of granularity. Therefore, the abstract model must be detailed enough to capture the relevant behavior of the system and should be done with a high level of confidence.

Formal methods are used to ensure a high level of confidence in a system behavior. More precisely, formal methods are used to specify the systems by building an abstract representation of the real system, which focuses on the requirements that the system should satisfy. The formal modeling describes the system using mathematical and logical theories. Then, we deploy formal verification on the formal model to prove the target properties.

Several techniques are employed to verify properties, starting from testing to simulations before achieving now the formal proving. Both testing and simulation are widely used in practice, more precisely in industrial applications, and their use has proven to be very useful. However, it is usually not possible to simulate or test all behaviors of a given system. Thus, we can rely on formal verification to address this behavioral coverage issue and prove the absence/presence of errors.

Two types of proof techniques exist: deductive, e.g., theorem proving [START_REF] Gallier | Logic for Computer Science: Foundations of Automatic Theorem Proving[END_REF] and algorithmic, e.g., model checking [START_REF] Clarke | Exploiting symmetry in temporal logic model checking[END_REF] [START_REF] Yu | Model checking tla + specifications[END_REF]. Theorem proving permits to establish the system's properties through mathematical reasoning. The theorem-proving techniques, while expressive, have limitations as they require extensive manual efforts in order to build proofs. Model checking permits to verify a system's properties by exploring all possible behaviors of a specification of this system with a limitation to face state explosion. We introduce next general formal notions before focusing on model checking, which we use to prove timing predictability-related properties over the hardware designs.

. Formal Notions

We present next some notions regarding formal modeling and verification.

Definition 1 (values, variables). We denote by V al a set of values, where a value is a data item and by V ar a set of variables.

A logic consists of a set of rules for manipulating formulas. We need to define the semantics to understand what the formulas and their manipulation mean. The semantics of our mathematical logic is defined in terms of state using the notation from [START_REF] Lamport | The temporal logic of actions[END_REF].

Definition 2 (state).

We define a state s as a mapping from state variables V ar to values V al, and we denote this by s(x) = v where x ∈ V ar and V ∈ V al.

The set of all states named the state space is denoted as St. The choice of states of a transition system, which describes how to pass from a state to another, depends on how much of that behavior needs to be observed in order to analyze a particular property of interest. The initial states correspond to the starting point on which we observe the system, and the next-relation includes all other possible transitions.

Definition 3 (transition system (TS)

Definition 4 (execution in a TS). We define the execution (also called behavior) of a transition system as a sequence of states (s 1 , s The diameter of a TS is the least number of steps to reach all reachable states (i.e., the states that belong to at least one initial execution).

Definition 5 (labelled transition system (LTS)).

We define a labelled transition system, the tuple (St t , I, Λ, → Λ ), where:

• St t is the set of states, • I ⊆ St t is the set of initial states, • Λ is a set of labels,
• → Λ is the transition relation that includes the set of labelled transitions.

Executions of an LTS are of the form (s 1 , a States and new states are linked with a relation called action.

Definition 7 (action). We define an action as a boolean-valued expression

between unprimed variables and primed variables. We say that action A is true on step s ⇒ t, or that s ⇒ t is an A step, if A assigns the value true to s ⇒ t

As an example, y = x ′ + 1 asserts that the value of y in a state is one greater than the value of x in the new state.

Definition 8 (validity). A validity of an action A, written as |=

A is that every step is an A step. Formally:

|= A ≜ ∀s, t ∈ St : s[[A]]t.
It is common to think of a system's execution as a series of actions. Thus reasoning about systems means reasoning about state sequences. Temporal logic is responsible for this type of reasoning.

Definition 9 (temporal formulas).

A temporal formula is made from elementary formulas (predicates and transitions) using boolean operators and the unary operator □ (read always). For example, if E1 and E2 are elementary formulas, then ¬E1 ∧ □(¬E2) and □(E1 ⇒ □(E1 ∨ E2)) are temporal formulas. Moreover, for any temporal formula F , let ♢F (read eventually) be defined by ♢F ≜ ¬□¬F A linear-time property is a requirement imposed on the traces (observable behaviors occurring during system runs) of a transition system, denoted by example with the set Traces(TS). In order to express linear-time properties, we can adopt specialized temporal logic, for instance, Linear Temporal Logic (LTL) or one of its variants. LTL formulas are expressed on infinite sequences of states where each point in time (state) has a unique successor based on a linear-time perspective. We are interested in a class of LTL properties, which are called invariants.

Definition 10 (linear-time property (LT)). We define a linear-time property

over the set of atomic predicates denoted by AP , as a subset of (P(AP )) ω , i.e., of the set of sequences whose elements are in P(AP ).

Let P = {(A 1 , A

. Model Checking Formal Verification Method

Model checking [START_REF] Clarke | Exploiting symmetry in temporal logic model checking[END_REF] is an automated approach used to verify that a model of the system satisfies a specification expressed as a property. The property defines the requirements requested for the expected behavior of the system. Model checking verifies by exploring the model's states allowed by the specification. Achieving the system abstraction and specification is a crucial step that may require system mastery and expertise in the methods used.

Once the system is modeled and the property is also defined, an investigation of whether the model satisfies the specification is performed, by exploring all possible executions of the system from its initial states. Then, the model checking automatically generates a counter-example when the property is not satisfied as an execution trace starting from the initial state to the state violating the invariants. Thus, the model-checking approach is performed on two main phases (modeling and specification verification). Two categories of model checking exist, explicit model checking [START_REF]The TLA+ Language and Tools for Hardware and Software Engineers[END_REF][START_REF] Holzmann | Explicit-State Model Checking[END_REF] and symbolic model checking [START_REF] Burch | Symbolic model checking: 1020 states and beyond[END_REF][START_REF] Mcmillan | Symbolic model checking: an approach to the state explosion problem[END_REF]. [START_REF]The TLA+ Language and Tools for Hardware and Software Engineers[END_REF] contains a description on explicit model checking as TLC.

Explicit Model Checking. Explicit model checking is often based on a state space exploration, where progress is made one state at a time, and each processed reachable state of the system is represented in memory explicitly. Explicit state model checking performs a depth-first or breadth-first search through the system's states, from a state to its successors. Therefore, all the states participating in the search are reachable from the initial state, which facilitates to evaluate the number of states encountered during the verification. The main drawback of explicit model checking is state space explosion: time and memory required to verify the system grows linearly with the number of its possible states. However, it scales better to harder verification problems than symbolic model checking [START_REF] Eisner | Comparing symbolic and explicit model checking of a software system[END_REF], since its configuration is explicit.

Symbolic Model Checking. To avoid the state-explosion issue in the model checking method, the symbolic category mitigates this problem through representing the system state space symbolically instead of explicitly. Symbolic model checking considers a state space encoding which is implicit, based on Boolean formulas, and examines sets of states in each step. The compressed representation of the state space is done using the binary decision diagrams (BDD) [START_REF] Andersen | An introduction to binary decision diagrams[END_REF] as one approach to symbolic model checking. BDDs are representations of Boolean functions that are compact. The reason why the state space explosion problem is mitigated is that space requirements for Boolean functions are exponentially smaller than for explicit representation.

. TLA+ Language

The abstract models that we aim to generate would be integrated into a procedure of the detection of timing anomalies. Thus, the need to model the cycle-accurate behavior of the generated micro-architecture models. Sev-eral tools exist for modeling the hardware architectures and verifying timing properties. We generate the formal models of the pipeline modeled as TLA+ specifications, and we use TLC, the explicit model checking tool, to explore the models and prove properties about timing anomalies.

TLA+ is a modeling language that offers a module system, the untyped set theory and predicate logic, making it appropriate for the specification of complex computational systems like computer architectures. The choice for TLA+ language is not coincidental but because of several semantic factors. Untyped set theory (and predicate logic) are aspects of the modeling language that allow for the specification of extensive state data. A further advantage of TLA+ is its advanced module system, which is based on interfaces, parameters, local declarations, etc. This system enables the precise development of abstract architecture models from smaller components.

Abstraction in TLA+ is ensured by temporal existential quantification, which hides unnecessary state elements. However, this is not supported by the TLC model checker. Moreover, refinement is natural in TLA+ and supported by ensuring stuttering invariance (i.e., execution steps that do not change the values of state variables of interest), which allows reasoning about the specification paths on different levels of granularity and temporal existential quantification to slice away the unnecessary state elements.

All the aforementioned concepts establish TLA+ as a unified logical language designed to specify both systems and their properties and verify, using the same specification, both a system and its possible refinements. Abstraction and refinement characteristics of TLA+ are more important in our timing properties verification purpose when we specify the system as a single formal specification which is then systematically refined. TLA+ is supported by an explicit model checker called TLC, which forms a powerful formal specification and verification framework.

A TLA+ model is organized in specifications built on two levels. The first level contains state and state transition formulas (i.e., system specification) and the second level constitutes the property evaluated on a sequences of states (i.e., system properties) to be verified. At the core of a TLA+ specification is the transition predicate, called action, which captures, using the primed notation, the state change, say for a variable x as x' = x + 1. If x is a record variable, its field f is accessed as x.f, and a partial record update is as [x EXCEPT!.f = v] (changing f to v and leaving the other fields of x unchanged). When the same field f keeps a value v, it is noted by f |-> v. Also, if a state variable x is not modified by an action, it is written in TLA+ as UNCHANGED «x».

To define an instance of module M inside another module, we use the construct INSTANCE M WITH, with the constants and the state variables of M being replaced by expressions of the instantiating module after the keyword WITH. Then, we can access operators op and transitions Act of the module M, with the operator "!". This operator gives access to these elements with M.op and M.Act. The Listing 2.5 illustrates an example of a simplified TLA+ specification to model an in-order processor design. We define the state variables representing the current cycle, the program, and the fetch pipeline stage. The specification Spec is defined through two operators: Init operator describes the initial state, while Next operator defines the next-state relation. We initialize the state variables to "0" and "empty" values in the initial state, where empty defines an empty content. Next is composed of several actions, in disjunction, where we update the current cycle (currCycle) and the first pipeline stage (_IF) in order to capture the execution of a program through the pipeline. TLA+ features expressions such as condition statements implemented with Formal verification is used to check the correctness of the properties. We specify the property to verify in Prop and then, the TLC model checker explores Spec and stops when the property is not verified, for instance, when the cycle reaches 50 (a counter-example is returned) or when the property is verified.

. Conclusion

We introduce the main elements we need in our workflow in Figure 4.1. We started by presenting a general background on hardware construction languages and highlighting their advantages in enabling reusability and customization. We specified our chosen hardware construction language and its compilation framework Chisel/FIRRTL in Section 2.1. Then, in Section 2.2, we introduced the main HDL design of processors related to the pipeline analysis phase. Finally, in Section 2.3, we detailed the formal modeling and verification methods and tools we will employ for timing properties proof in our thesis work. From this preliminary presentation, we detail in the next chapter the use of these elements for the purpose of generating pipeline models to verify timing properties.

-State of the Art

Verifying the timing properties of safety-critical systems requires not only models of the critical applications but also models of the hardware that executes these applications. The hardware models are in general considered at the micro-architecture level. These micro-architecture models are generally developed from processor manuals. Recent trends in hardware design and ISA distribution led to more processor code being made available and supported by the emergence of new design languages with a high-level abstraction, which makes the automatic generation of micro-architecture models possible.

In this section, we introduce related works on constructing microarchitecture models from code of hardware designs. Thus, several aspects should be considered. First, we present various works addressing the core of our research problem, that of pipeline modeling, in Section 3.1, Second, we provide an overview of related work on hardware description languages (HDLs), in Section 3.2, the type of languages we analyze to construct the pipeline models. In this section, we also highlight the main advantages of employing Hardware Construction Languages (HCLs) over standard design languages when describing the semantics of hardware designs. Third, since our approach is based on code-level analysis, we use several techniques for code exploration to develop our analysis. Section 3.3 details related work on program analysis-based techniques and algorithms to be adapted for our analysis. Finally, we highlight further in Section 3.4 some related work on formal verification of timing properties by model checking. Our pipeline models are formalized and used in the verification of timing properties using model checking. We capture in this section the use of model checking to verify timing properties. We have a focus on their existing pipeline models in order to generate, with our thesis work, suitable models for model checking verification.

. Building Pipeline Models from Hardware Designs

Building pipeline models from hardware designs was the subject of several research works, however different in their purpose, technique employed, and hardware description language of the design. The works [START_REF] Charvát | HADES: microprocessor hazard analysis via formal verification of parameterized systems[END_REF][START_REF] Mir | Modeling and verification of embedded systems using cadence smv[END_REF][START_REF] Mukherjee | Hardware verification using software analyzers[END_REF] aim to generate formal pipeline models for functional verification purposes. Other kind of works [3, 4, 9-11, 14, 45-47] focus on constructing pipeline models for WCET applications. The pipeline model construction could be done manually from processor manuals [9-11, 14, 45-47] or built from HDL designs [3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF]. Finally, the works [START_REF] Kroening | Automated pipeline design[END_REF][START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF][START_REF] Gorius | Spechls: Speculative accelerator design using high-level synthesis[END_REF] address a synthesis problem, with [START_REF] Gorius | Spechls: Speculative accelerator design using high-level synthesis[END_REF] that focus on high-level synthesis and [START_REF] Kroening | Automated pipeline design[END_REF][START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF] as they synthesize automatically a pipelined implementation, automating the design from a sequential implementation.

We start with works [START_REF] Charvát | HADES: microprocessor hazard analysis via formal verification of parameterized systems[END_REF][START_REF] Mir | Modeling and verification of embedded systems using cadence smv[END_REF][START_REF] Mukherjee | Hardware verification using software analyzers[END_REF] on pipeline models for functional verification purposes. A first work in automatically generating a formal pipeline is presented in [START_REF] Charvát | HADES: microprocessor hazard analysis via formal verification of parameterized systems[END_REF]. This paper introduces the HADES tool, where the pipelinebased processors are represented as graphs, with the user being required to identify the architectural resources such as registers and memory ports. Then, the HADES tool identifies the pipeline stages and generates the pipeline model as a graph which is then used to deal with data hazards. Indeed, after having generated the pipeline graph, the HADES tool identifies the pipeline stages using a data flow analysis. Then it checks the correctness of the instruction execution through the identified pipeline stages. Furthermore, the abstract pipeline models generated with the HADES tool include the forwarding mechanism, as HADES concentrates on data hazards. It addresses the absence of problems caused by data hazards on microprocessors with a single pipeline and in-order execution.

Furthermore, generating the formal model from hardware designs is a recurrent task in the hardware compilation field. However, most works focus on RTL-level designs, described using standard hardware description languages (VHDL, Verilog) [START_REF] Charvát | HADES: microprocessor hazard analysis via formal verification of parameterized systems[END_REF][START_REF] Mir | Modeling and verification of embedded systems using cadence smv[END_REF]. Their micro-architecture designs are modeled using these kinds of languages. The work in [START_REF] Mir | Modeling and verification of embedded systems using cadence smv[END_REF] investigates a formal verification system for hardware designs called Cadence SMV [START_REF] Mcmillan | Cadence smv[END_REF]. In fact, the Cadence-SMV uses Verilog to express the system model. It uses the Verilog design as input to generate the SMV design. It is constructed by integrating the micro-controller RTL and embedded software assembly code levels. Then, the model is validated, and the properties to verify are proved by conducting a model checking tool.. Moreover, the work in [START_REF] Mukherjee | Hardware verification using software analyzers[END_REF] addresses the formal property checking for the hardware designs. This work aims to provide an automatic verification technique for Verilog designs as it builds hardware models from the input designs developed in Verilog. The model is a transition system at the RTL level. Verilog design is translated first to ANSI-C programs based on a synthesis semantics interpretation of the Verilog code, then to a common representation (IR) for the goal of formal verification with various technologies. The aim is to increase the performance and scalability in the verification since the new representation allows the application of a range of modern analysis techniques for software.

We continue our survey on pipeline modeling with works addressing pipeline models in the context of the WCET analysis [3, 4, 9-11, 14, 45-47].

The works in [3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] address the goal of analyzing processor design code [3] and determining micro-architecture models for the WCET analysis [START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF]. Moreover, these works [3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] present a framework based on static analysis of hardware designs. The hardware design, which is developed in the VHDL language, is transformed into an intermediate control-flow representation on which an abstract interpretation is built, for each basic block of the input program.

Figure 3.1 illustrates the VHDL static analysis framework, which translates a VHDL code into a sequential program with an arbitrary execution order of its processes. The processes corresponding to functions, procedures, assignment signals, loops, etc., are transformed into routine constructs specified in the intermediate representation (CRL2) of the aiT timing analyzer. Then, a static analysis is performed through the program analyzer generator (PAG) on the intermediate VHDL representation, for timing analysis. The results of [3] are applied in [START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] to determine microarchitecture models using a semi-automatic procedure based on program slicing. More precisely, program slicing is used to eliminate parameterized features of the design (i.e., for conditional compilation), and certain signals (e.g., for events and interrupts) are manually initialized. Thus, these signals never change value and can be removed easily through dead-code elimination and control refinements. The approach in [START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] performs value analysis to approximate register and memory contents, aiming to simplify the original VHDL design (i.e., changing pseudo-VHDL processes) to a datapath representation with accurate timing. The approach depends on correctly identifying the control path information, which is not fully automated.

This approach is based on the framework from [3] to perform dead-code elimination, control signal refinements, and datapath elimination. These applied transformations reduce the code size of the VHDL design. Then, abstractions are implemented concerning the memory, the types of variables, and the registers where the analysis focuses on the time of storing values and ignores the value stored. Figure 3.2 details the main abstractions applied to the VHDL design in order to get timing models. The approach proves its efficiency for simple architecture, such as the DLX pipeline, and failed for more complex architecture, like LEON2, an industry processor. Indeed, some VHDL statements are not supported in their modeling as composite data structures and wait statements. Furthermore, the processor state abstractions are manual and dependent on the particular processor and its complexity. Pipeline models which are not extracted from HDL processor designs but relevant to the WCET analysis are addressed in [9-11, 14, 45-47].

State of the art static timing analyzers such as aiT [START_REF] Langenbach | Pipeline modeling for timing analysis[END_REF][START_REF] Ferdinand | Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, ser[END_REF], Otawa [START_REF] Ballabriga | OTAWA: an open toolbox for adaptive WCET analysis[END_REF], Heptane [START_REF] Hardy | The heptane static worst-case execution time estimation tool[END_REF] or Chronos [START_REF] Li | Chronos: A timing analyzer for embedded software[END_REF] consider architecture models (of caches or pipelines) and use static analysis to characterize their timing. These architecture models are usually handcrafted using mainly the processor documentation as input and sometimes validated against hardware simulators for conformance. Otawa [START_REF] Ballabriga | OTAWA: an open toolbox for adaptive WCET analysis[END_REF] is a toolbox for the WCET analysis integrating analyses for both program and architecture. Listing 3.1 presents a snapshot of the micro-architecture configuration file in the XML format. First, the pipeline width and length are specified. Then, the pipeline model is presented with its stages. Each stage is characterized with its name specified in id field, lines 6, 11, 16, and 34 in Listing 3.1. Number of functional units and their latencies, lines 21-33, binding of instruction categories to the functional units. The pipeline model is not very rich. Its description focuses more on the pipeline stages level. In contrast, the pipeline mechanisms, such as forwarding and stalling, are described later in the OTAWA code. They are resolved at the program level, where the instruction dependencies are preliminarily studied.

Listing 3.1 -OTAWA XML file for hardware abstraction. Heptane [START_REF] Hardy | The heptane static worst-case execution time estimation tool[END_REF] and Chronos [START_REF] Li | Chronos: A timing analyzer for embedded software[END_REF] analyzers are built on top of the freely available SimpleScalar simulator [START_REF] Burger | The simplescalar tool set[END_REF]. SimpleScalar is a cycle-accurate architectural simulator that allows the user to model a variety of processor platforms in software. Figure 3.3 illustrates the structure of Chronos tool to compute WCET bounds.

Heptane/Chronos compute WCET using static analysis at the binary code level. The input program is presented in basic block windows. These tools perform micro-architecture modeling, which yields time bounds for each basic block's execution. Each instruction in the basic block has a time interval at which it can start/finish the execution. Then, tools compute the dependence between instructions and the stalling delay to be added to the basic block time counts to refine the estimates. Thus, the forwarding and stalling mechanisms are not explicitly coded, and the WCET bounds are determined, including the program analysis and the pipeline modeling.

As such, the work in [START_REF] Bai | Improving the performance of WCET analysis in the presence of variable latencies[END_REF] considers basic blocks to be mapped into the pipeline stages in order to define an execution graph, which is then used to compute the WCET bound. WCET computation in [START_REF] Bai | Improving the performance of WCET analysis in the presence of variable latencies[END_REF] is enhanced by considering variable latencies in instruction sequences. The approach exploits the fact that several latency combinations produce the same WCET and employs Binary Decision Diagrams to improve the WCET analysis' scalability. The work in [START_REF] Li | Modeling out-of-order processors for WCET analysis[END_REF] also models an out-of-order superscalar processor for the WCET analysis. The approach is based on an execution graph that integrates both the micro-architecture models and the program-level analysis defined on basic blocks. The execution graph captures data dependencies, resource contentions and degree of superscalarity. Each node in the execution graph is associated with the latency interval of the corresponding pipeline stage. The estimation technique proceeds by a fixed-point analysis of the time intervals at which the instructions enter/leave a pipeline stage in order to avoid exhaustive enumeration of instruction schedules. Then, the basic block estimates are combined using Integer Linear Programming (ILP) to produce the program's WCET estimate.

Other related works on pipeline modeling address a synthesis problem, in [START_REF] Kroening | Automated pipeline design[END_REF][START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF][START_REF] Gorius | Spechls: Speculative accelerator design using high-level synthesis[END_REF]. The paper [START_REF] Gorius | Spechls: Speculative accelerator design using high-level synthesis[END_REF] proposes a SpecHLS, a source-to-source compiler framework that performs a high-level synthesis for speculative hardware structure. They focus on speculative loop pipelining for arbitrary control flow and memory speculation patterns. The framework takes as input C code and produces transformed C code that supports speculative loop pipelining. The C code is transformed into an intermediate representation (IR). Then, the analyses are explored on this representation. The approach is also applied for accelerator-based in-order pipelined RISC-V CPU and shows their performance improvement for speculative execution. Furthermore, [START_REF] Kroening | Automated pipeline design[END_REF][START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF] create automatically the processor pipeline model from a sequential abstract model based on registers. More specifically, their goal is to synthesize pipeline designs from sequential representations, starting from simple designs [START_REF] Kroening | Automated pipeline design[END_REF] to more complex variants [START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF]. The approach in [START_REF] Kroening | Automated pipeline design[END_REF] has two phases. It first identifies the number of pipeline stages to create a sequential pipeline imple-mentation based on the forward dependencies. Then it adds, in the second phase, the forwarding and interlock logic required for a pipelined execution.

Furthermore, the work [START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF] models the datapath as a transactional specification to synthesize automatically an in-order pipelined implementation. The transactional specification considers the datapath as executing one transaction at a time. It captures an abstract datapath, where its execution semantics is interpreted as a sequence of "transactions". Transactions consist of state elements that include the combinatorial and sequential logics, and next-state compute operations and updates through the logic blocks. The analysis is based on an assignment algorithm where each module (or interface in the case of a state element) is assigned to the corresponding pipeline stage.

Summary. Several works have been presented in this section to describe the techniques of building pipeline models from HDL designs. Hardware designs, in general, and pipeline designs, in particular, can be expressed with various kinds of hardware languages. We present next works on HDL languages with a highlight of their semantics and their advantages/shortcomings for the purpose of constructing abstract hardware models which could be used to verify timing properties.

. Semantics of High/Low-Level Hardware Languages

Hardware description languages (HDLs) allow the specification of hardware design's functional and temporal behavior. We distinguish between mainstream, traditional HDLs with low abstraction levels as VHDL and Verilog, and more expressive languages, capable of high-level of abstraction, such as Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF], BlueSpec [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF], SAFL [START_REF] Mycroft | Hardware synthesis using SAFL and application to processor design[END_REF], Lava [START_REF] Bjesse | Lava: Hardware design in haskell[END_REF], etc. These languages are known as Hardware Construction Languages (HCLs). HCLs can be seen as domain-specific languages that leverage the power of high-level languages like Python, Scala, etc., to build efficient hardware generators that produce, in the end, synthesizable VHDL or Verilog code.

Traditional HDL languages are declarative and provide very little reflexivity over the circuit being described and could require an appropriate abstraction level in order to generate a formal model. More precisely, these work [START_REF] Gordon | The Semantic Challenge of Verilog HDL[END_REF][START_REF] Meredith | A formal executable semantics of verilog[END_REF][START_REF] Gordon | Relating event and trace semantics of hardware description languages[END_REF] address this aspect by presenting the semantic challenges of the Verilog language. Recently, the hardware designers started to move towards hardware construction languages which are convenient to facilitate formal verification and synthesis [START_REF] Greaves | Layering rtl, safl, handel-c and bluespec constructs on chisel hcl[END_REF] such as SAFL [START_REF] Mycroft | Hardware synthesis using SAFL and application to processor design[END_REF], Kami [START_REF] Choi | Kami: a platform for high-level parametric hardware specification and its modular verification[END_REF], and Bluespec [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF], and domain-specific languages (DSLs) [START_REF] Truong | A golden age of hardware description languages: Applying programming language techniques to improve design productivity[END_REF] as Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF], Lava [START_REF] Bjesse | Lava: Hardware design in haskell[END_REF] and CλaSH [START_REF] Baaij | C?ash: Structural descriptions of synchronous hardware using haskell[END_REF]. Finally, there are high-level HDL languages designed for specific types of hardware like accelerators, e.g. Spacial [START_REF] Koeplinger | Spatial: a language and compiler for application accelerators[END_REF] and Calyx [START_REF] Nigam | A compiler infrastructure for accelerator generators[END_REF]. Then, we give an overview of the intermediate representations compiled from the hardware construction languages through the hardware compilation frameworks [START_REF] Izraelevitz | Reusability is firrtl ground: Hardware construction languages, compiler frameworks, and transformations[END_REF][START_REF] Schuiki | LLHD: a multi-level intermediate representation for hardware description languages[END_REF]. We then describe work on comparative studies [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF][START_REF] Pan | Towards gradually typed hardware description languages[END_REF][START_REF] Im | Comparative analysis between verilog and chisel in RISC-V core design and verification[END_REF][START_REF] Lennon | A comparative study of chisel for fpga design[END_REF][START_REF] Bruant | system)verilog to chisel translation for faster hardware design[END_REF] regarding the general semantics of hardware construction languages and their main advantages over mainstream HDLs.

We start with semantics challenges of Verilog. The following works [START_REF] Gordon | The Semantic Challenge of Verilog HDL[END_REF][START_REF] Meredith | A formal executable semantics of verilog[END_REF][START_REF] Gordon | Relating event and trace semantics of hardware description languages[END_REF] consider Verilog as the driving example of a hardware description language widely employed in industrial designs. The work in [START_REF] Gordon | The Semantic Challenge of Verilog HDL[END_REF] describes the Verilog language and addresses the variety of interesting semantic challenges that Verilog presents. The first challenge is that the studied Verilog semantics in [START_REF] Gordon | The Semantic Challenge of Verilog HDL[END_REF] does not include value sizing and is not executable, making specifying what output a given program should produce more difficult. Also, a Verilog semantic challenge concerns the development of the language's smaller and traceable semantics and the synthesis formalization to prove the equivalence between the hardware structures generated and the behavioural source. Another semantic challenge concerns the simulation cycle semantics and how to integrate it into the formalization of Verilog.

Then, the works in [START_REF] Meredith | A formal executable semantics of verilog[END_REF][START_REF] Gordon | Relating event and trace semantics of hardware description languages[END_REF] take into consideration these challenges and propose formal semantics of Verilog towards providing a concise reference of the official language standard and aiding the development of Verilog-based verification tools. One of these semantics, proposed in [START_REF] Meredith | A formal executable semantics of verilog[END_REF] is based on the functional programming style and covers the Verilog functionalities (e.g., its non-determinism) in an executable framework, creating the possibility to test Verilog code. However, the semantics [START_REF] Meredith | A formal executable semantics of verilog[END_REF] does not deal with events and simulation traces. These features are considered in [START_REF] Gordon | Relating event and trace semantics of hardware description languages[END_REF], where the focus is on the formal simulation semantics of Verilog. More precisely, this work [START_REF] Gordon | Relating event and trace semantics of hardware description languages[END_REF] presents a formal semantics of traces (the sequence of states in a simulation) and events in HDLs and, in particular, in the Verilog language. In order to achieve this goal, their work proceeds in three main steps. First, it presents the syntax of Verilog linked to time constraints, for instance, events, clocks, etc. Second, it presents Verilog in the simple form of a pseudocode, in order to reduce this language constructions to a canonical form and to simplify the formalization and the verification. Finally, it presents the formal semantics of traces through a definition of traces for a combinational logic and for a sequential logic and then a combination of the two, taken at the circuit level.

In summary, Verilog [START_REF] Gordon | The Semantic Challenge of Verilog HDL[END_REF] poses a variety of interesting semantic challenges that are considered in [START_REF] Meredith | A formal executable semantics of verilog[END_REF][START_REF] Gordon | Relating event and trace semantics of hardware description languages[END_REF], however with this language (or VHDL) the circuit details are fixed early in the design and the flexibility is lost when further modifications are required. Thus, hardware designers seek high-level descriptions to synthesize hardware.

In the following, we overview the semantics of more expressive hardware languages, called hardware construction languages. As such, we enumerate SAFL [START_REF] Mycroft | Hardware synthesis using SAFL and application to processor design[END_REF], Kami [START_REF] Choi | Kami: a platform for high-level parametric hardware specification and its modular verification[END_REF] and Bluespec [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF] as languages designed to facilitate the formal verification and Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF], Lava [START_REF] Bjesse | Lava: Hardware design in haskell[END_REF] and CλaSH [START_REF] Baaij | C?ash: Structural descriptions of synchronous hardware using haskell[END_REF] as DSLs.

The work in [START_REF] Mycroft | Hardware synthesis using SAFL and application to processor design[END_REF] describes SAFL, a high-level hardware description language used in circuit design. In particular, SAFL is expressive to describe processors and their functional properties and uses transformations to change the design. For example, SAFL provides transformations to adjust the source program's area-time consumption and optimize the code without altering its complex structure. Thus, the main advantage of SAFL is that it is resourceaware.

The work in [START_REF] Choi | Kami: a platform for high-level parametric hardware specification and its modular verification[END_REF] introduces Kami, a platform for high-level parametric hardware specifications. Kami is based on Coq [START_REF] Roe | sifive/kami[END_REF] to specify and verify hardware designs, then uses Coq's code extraction to generate code for FPGAs. A hardware design in the Kami language is presented as a set of modules as it addresses complete circuits through small components that are combined. For example, Kami is used to specify, implement and verify realistic multiprocessor systems with design functionality covering the pipeline and the simultaneous memory/cache access. The main advantage of the Kami framework is that it can generate HDL code for FPGAs from the formalization.

The work in [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF] presents Bluespec, a high-level hardware description language that is essentially a variant of SystemVerilog. It is a language that simplifies and promotes formal proof while preserving the compiled circuit's performance. A hardware design in Bluespec is specified in atomic rules and guaranteed that rules appear to execute atomically one at a time, controlled by a scheduler. This scheduler expresses the synthesizable behavior as it is automatically generated to avoid race conditions between the atomic rules. The main advantage of Bluespec is its semantics based on rules which lead to naturally generating HDL code for FPGAs.

All these languages presented in [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF][START_REF] Mycroft | Hardware synthesis using SAFL and application to processor design[END_REF][START_REF] Choi | Kami: a platform for high-level parametric hardware specification and its modular verification[END_REF]] are considered recent hardware construction languages designed for synthesis and functional programming. SAFL [START_REF] Mycroft | Hardware synthesis using SAFL and application to processor design[END_REF] is best described as a synthesis rather than a construction language, while Bluespec [START_REF] Bourgeat | The essence of bluespec: A core language for rule-based hardware design[END_REF] and Kami [START_REF] Choi | Kami: a platform for high-level parametric hardware specification and its modular verification[END_REF] are generally employed for formal proof. Furthermore, Bluespec has adapted imperative features and a syntax that resembles Verilog. In addition, Bluespec re-implements the functional language itself with its own syntax and parser. However, embedded languages in a DSL avoid having to re-implement a parser which greatly increases productivity. Furthermore, they are severely limited in practical applicability [START_REF] Greaves | Layering rtl, safl, handel-c and bluespec constructs on chisel hcl[END_REF].

There are hardware construction languages that are embedded in a powerful host language, the so-called domain-specific languages (DSLs) for hardware. The work in [START_REF] Truong | A golden age of hardware description languages: Applying programming language techniques to improve design productivity[END_REF] surveys such DSLs providing a vision that combines a meta-programmed host language with a core embedded hardware description language used as the basis for many domain-specific languages. Further-more, this combination provides an abstraction that enables code reuse and improves programs' correctness. Several DSLs on hardware designs [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF][START_REF] Bjesse | Lava: Hardware design in haskell[END_REF][START_REF] Baaij | C?ash: Structural descriptions of synchronous hardware using haskell[END_REF] exist in the literature.

Lava [START_REF] Bjesse | Lava: Hardware design in haskell[END_REF] and CλaSH [START_REF] Baaij | C?ash: Structural descriptions of synchronous hardware using haskell[END_REF] are two hardware construction languages embedded in Haskell a functional programming language that focuses on the hardware's structural representation. These languages support high-level programming features such as polymorphic types and higher-order functions, besides support for simulation and circuit synthesis. Lava descriptions can be interfaced with formal verification tools. CλaSH differs from Lava as the description contains a rich control structure. The control structure contains the case-expressions and pattern matching as specified with Haskell's choice elements. These elements are synthesized into the choice elements in the eventual circuit. Thus, they can be best specified in CλaSH than possible within Lava, and hence are less error-prone.

Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF] is a DSL language in Scala. Chisel benefits from this integration as Scala is expressive, combining object-oriented and functional abstraction styles, and allows the encoding of a flexible hardware library. Furthermore, this embedding brings several other advantages like avoiding re-implementing a parser and having free access to all Scala libraries, leading to great productivity. Various aspects of the syntax and the semantics of Chisel are discussed at the end of this section, where we present several comparative studies as well as in the next chapters.

We continue our survey with another kind of hardware description languages which are not generic but specialized for hardware accelerators in [START_REF] Koeplinger | Spatial: a language and compiler for application accelerators[END_REF][START_REF] Nigam | A compiler infrastructure for accelerator generators[END_REF]. Spacial [START_REF] Koeplinger | Spatial: a language and compiler for application accelerators[END_REF] is a language and compiler framework for higher-level descriptions of application accelerators. It is developed to support performanceoriented hardware designs implemented on reconfigurable spatial architectures, including FPGAs. Indeed, it simplifies the accelerator design process, allowing the development, testing and optimizing hardware accelerators. Calyx [START_REF] Nigam | A compiler infrastructure for accelerator generators[END_REF] is an intermediate language to compile high-level programs into hardware design. Calyx combines software to represent the control flow of a design with hardware as a structural language for hardware modules. The Calyx compiler optimizes the programs and emits synthesizable RTL.

The compilation chains for high-level HDLs also propose intermediate languages to handle the semantics gap with respect to low-level Verilog and VHDL. Moreover, developing automated techniques for analyzing such HDL designs becomes tantamount to working with both the high-level HDL languages as well as with language transformation (i.e., compilation) issues. For example, the work in [START_REF] Schuiki | LLHD: a multi-level intermediate representation for hardware description languages[END_REF] proposes an intermediate-language representation named LLHD, which is inspired by LLVM IR, thus, in the SSA form. LLHD plays similar roles in a hardware compilation chain as FIRRTL [START_REF] Izraelevitz | Reusability is firrtl ground: Hardware construction languages, compiler frameworks, and transformations[END_REF]; for example, it helps to integrate compilation passes.

We continue with papers that focus on the comparative studies between hardware construction languages and traditional hardware description languages. Various research studies [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF][START_REF] Pan | Towards gradually typed hardware description languages[END_REF][START_REF] Im | Comparative analysis between verilog and chisel in RISC-V core design and verification[END_REF][START_REF] Lennon | A comparative study of chisel for fpga design[END_REF][START_REF] Bruant | system)verilog to chisel translation for faster hardware design[END_REF] have been carried out on Chisel to demonstrate its efficiency over other existing HDL languages. While low-level hardware description languages VHDL and Verilog are still used in industry, their age and original intention put them behind current high-level languages in terms of productivity and flexibility [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF][START_REF] Pan | Towards gradually typed hardware description languages[END_REF]. The work in [START_REF] Pan | Towards gradually typed hardware description languages[END_REF] reports the importance of static type checks of hardware generators in high-level languages compared to existing HDLs. HCL languages allow static type checking of a generator to discover potential design issues early in the design cycle. Furthermore, they need to support sophisticated hardware generators provided in high-level languages. The paper [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF] details these properties by enhancing the main features of Chisel languages and compares its advantages with VHDL language in terms of productivity and code size. We present next these properties highlighted in [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF].

First, Chisel features generate predefined blocks [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF] in order to simplify hardware design by providing parameterization for common hardware. Second, its datatype structure makes interfacing modules easier, allowing code reuse. These datatypes will be explained in detail in Section 4.2. Finally, Chisel benefits from the high-level programming features of Scala language, such as abstract functions, polymorphism, etc. These concepts are not presented in VHDL language, which could lead to duplicated code for similar functionality. However, the work in [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF] highlighted that the Chisel language is still in early development, which makes it not yet suitable for use in industry. At that moment, it was still under development and suggested a new stable syntax and documentation.

We continue with works in [START_REF] Im | Comparative analysis between verilog and chisel in RISC-V core design and verification[END_REF][START_REF] Lennon | A comparative study of chisel for fpga design[END_REF] related to benchmark studies between low-level and high-level HDLs, especially between Verilog and Chisel language. The comparison metrics include the source code density, the synthesizer circuit area, the RTL simulation runtime [START_REF] Im | Comparative analysis between verilog and chisel in RISC-V core design and verification[END_REF], design flow runtime and speed of coding through a range of FPGA design components [START_REF] Lennon | A comparative study of chisel for fpga design[END_REF]. High-level programming features in Scala languages allow Chisel designers to reduce the source code lines. They can reduce codes by using compound types instead of typing every signal in Verilog and employ functions to describe hardware circuits as, for example, pipelines. Chisel improves over Verilog in code maintainability and scalability. It can also efficiently detect architecture issues and generate direct warning and error messages in complex designs [START_REF] Lennon | A comparative study of chisel for fpga design[END_REF].

Summary. This section has detailed works related to hardware languages, including the traditional HDLs and HCLs languages. We have focused on their semantics and their significant differences for the goal of building pipeline models. Building pipeline models relies primarily on code analysis. We present the following works on code analysis techniques, focusing on those that can be exploited in our approach.

. Code Analysis Approaches

Analyzing open-source hardware designs means, on the one hand, integrating into the analysis the semantics of the HDL used in the design and, on the other hand, understanding what the design is about, for example, that is a processor design. Design complexity and library reuse make working on the whole design difficult, therefore, the need for structured code-level design and analysis techniques is necessary. Several code analysis techniques have been used in literature to address various problems in design, simulation, testing and formal verification. We group these works into general-purpose analysis techniques and code-level HDL-specific techniques. For instance, in the general-purpose category, we mention the works on the abstract syntax tree (AST) [START_REF] Neamtiu | Understanding source code evolution using abstract syntax tree matching[END_REF][START_REF] Yang | Identifying syntactic differences between two programs[END_REF], while other works use dependence graphs [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demanddriven interpretation of imperative languages[END_REF][START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF][START_REF] Kim | Malware detection based on dependency graph using hybrid genetic algorithm[END_REF]. Furthermore, program slicing [START_REF] Clarke | Program slicing of hardware description languages[END_REF][START_REF] Tip | A survey of program slicing techniques[END_REF] is among these techniques that intend to reduce the program and work on the relevant code portions. Finally, static analysis [START_REF] Bertrane | Static analysis by abstract interpretation of embedded critical software[END_REF][START_REF] Xavier Rival | Introduction to Static Analysis An Abstract Interpretation Perspective[END_REF] is also used to analyze code for several purposes. For the HDLspecific methods, we intend to present the application of these techniques on hardware designs. As such, the works in [START_REF] Clarke | Program slicing of hardware description languages[END_REF][START_REF] Vasudevan | Improved verification of hardware designs through antecedent conditioned slicing[END_REF] address program slicing applications, while the works in [START_REF] Sharp | Soft scheduling for hardware[END_REF][START_REF] Athavale | Code coverage of assertions using RTL source code analysis[END_REF][START_REF] Li | Sapper: a language for hardware-level security policy enforcement[END_REF][START_REF] Li | Caisson: a hardware description language for secure information flow[END_REF] propose applications of the static analysis.

We start first with an overview of general-purpose analysis techniques. Analyzing the source program code based on analyzing the corresponding AST has been developed in different research works [START_REF] Neamtiu | Understanding source code evolution using abstract syntax tree matching[END_REF][START_REF] Yang | Identifying syntactic differences between two programs[END_REF]. These works present an application example of analyzing C programs, more precisely, to monitor code evolution by comparing the source code of different versions of the code under analysis. This approach is based on analyzing the partial AST matching in order to identify the significant changes (additions, deletions of global variables, types, and functions) between code versions and report various statistics on dynamic software updates. The approach traverses, in parallel the two AST produced from the programs parsing and collects the construction elements as type and name to build a mapping. The approach in [START_REF] Yang | Identifying syntactic differences between two programs[END_REF] also begins by finding function names that are common between program versions and do not change very often as the beginning assumptions. Then it goes through the AST (function body) to identify changes in function semantics.

We continue with works [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demanddriven interpretation of imperative languages[END_REF][START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF][START_REF] Kim | Malware detection based on dependency graph using hybrid genetic algorithm[END_REF] that use dependence graphs to analyze code. The work in [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demanddriven interpretation of imperative languages[END_REF] presents an intermediate representation for programs based on the Program Dependence Graphs (PDGs) [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF] which is used to ana-lyze the data/control flows in programs. PDGs provide a unifying framework that makes data and control dependence explicit for each program operation and thus it permits an efficient and powerful program transformation. The intermediate representation in [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demanddriven interpretation of imperative languages[END_REF] presents various benefits to the program analysis and a basis for program optimization. Figure 3.4 illustrates a control dependence graph based on the control flow graph and dominators. A control flow graph is a directed graph G augmented with a unique entry node Start and a unique exit node Stop such that each node has at most two successors. The two successors of nodes have attributes "T" (true) and "F" (false) associated with the outgoing edges in the usual way. For each node N, we assume that there exists a path from Start to N and a path from N to Stop. We construct the control-dependent graph through the following definition. Let X and Y be nodes in G. Y is control dependent on X if there exist a directed edge P from X to Y with any Z post-dominated by Y and X is not post-dominated by Y. We can notice that a node V is post-dominated by a node W in G, if every directed path from V to STOP (not including V) contains W. Region nodes R1 through R6 and Entry have been inserted to more accurately represent control flow dependencies, especially in the presence of loops and conditional structures. The control dependence graph is built using a control flow graph and dominators in the approach [START_REF] Allen | Control flow analysis[END_REF][START_REF] Aho | Compilers: Principles, Techniques, and Tools, ser. Addison-Wesley series in computer science / World student[END_REF]. Another work [START_REF] Kim | Malware detection based on dependency graph using hybrid genetic algorithm[END_REF] related to the dependency graph implementation for the goal of detecting polymorphism computer malware. Polymorphism malware is typically based on malware viruses with different signatures. They are challenging to detect since their signatures still need to be analyzed when they first appear. Thus, the approach is based on comparing the dependency graph of the target file with all the database virus dependency graphs to determine whether this target file is a polymorphic variant of existing detected malware.

Static analysis [START_REF] Bertrane | Static analysis by abstract interpretation of embedded critical software[END_REF][START_REF] Xavier Rival | Introduction to Static Analysis An Abstract Interpretation Perspective[END_REF][START_REF] Cousot | Abstract interpretation of graphs[END_REF] is one of the most popular approaches employed when checking properties at code level. [START_REF] Cousot | Abstract interpretation of graphs[END_REF] describes the use of the static analysis fixpoint approach to solve the path problems in graphs. The paper [START_REF] Bertrane | Static analysis by abstract interpretation of embedded critical software[END_REF] presents the application of semantic-static analysis to check errors in software design based on abstract interpretation. Semantic-static analysis can be used to prove properties at various levels of the software designs and always covers all the program executions as static analysis works on the control flow graph. The properties of interest in [START_REF] Bertrane | Static analysis by abstract interpretation of embedded critical software[END_REF] are the run-time errors in the code. A detailed presentation of static analysis and its applications can be found in [START_REF] Xavier Rival | Introduction to Static Analysis An Abstract Interpretation Perspective[END_REF]. Program slicing [START_REF] Clarke | Program slicing of hardware description languages[END_REF][START_REF] Tip | A survey of program slicing techniques[END_REF] is a static analysis technique that automatically extracts portions of programs according to an objective (also known as slicing criterion). Slicing provides a program reduction that simplifies the original code and facilitates its formal verification. The work in [START_REF] Tip | A survey of program slicing techniques[END_REF] presents an overview of algorithms for program slicing covering both static and dynamic approaches as well as language features like procedures, data types, pointers, etc., as data and control flow graphs.

We continue with works in [START_REF] Clarke | Program slicing of hardware description languages[END_REF][START_REF] Vasudevan | Improved verification of hardware designs through antecedent conditioned slicing[END_REF][START_REF] Sharp | Soft scheduling for hardware[END_REF][START_REF] Athavale | Code coverage of assertions using RTL source code analysis[END_REF][START_REF] Li | Sapper: a language for hardware-level security policy enforcement[END_REF][START_REF] Li | Caisson: a hardware description language for secure information flow[END_REF] related to HDL-specific code-level analysis. More precisely, the works in [START_REF] Clarke | Program slicing of hardware description languages[END_REF][START_REF] Vasudevan | Improved verification of hardware designs through antecedent conditioned slicing[END_REF] present implementations of program slicing for VHDL designs. The work in [START_REF] Clarke | Program slicing of hardware description languages[END_REF] presents a slicing tool that automatically decomposes programs based on data and control flow analysis, using PDGs, in order to construct sliced programs. This work aims to deal with the concurrent constructs in the VHDL language. The approach maps VHDL constructs into constructs of other traditional procedural languages such as C and Ada languages. The approach relies on the VHDL semantics in a way that ensures that all the VHDL program traces, which are parallel, are valid for the corresponding sequential program. The work in [START_REF] Vasudevan | Improved verification of hardware designs through antecedent conditioned slicing[END_REF] extends the static program slicing to an improved variation called conditioned slicing. Conditioned slicing is an abstraction technique used for hardware verification that adds conditions to the slice in order to produce a smaller and more significant abstraction than static slicing. It specifies some initial states of interest in the slicing criterion for hardware verification. The states rely on the property to verify to apply conditioned slicing to Verilog code. The resultant conditional slices are more precise and relevant for the verification and also reduce the size of the verification state space.

The works in [START_REF] Sharp | Soft scheduling for hardware[END_REF][START_REF] Athavale | Code coverage of assertions using RTL source code analysis[END_REF][START_REF] Li | Sapper: a language for hardware-level security policy enforcement[END_REF][START_REF] Li | Caisson: a hardware description language for secure information flow[END_REF] focus on using static analysis on HDL designs. The work in [START_REF] Sharp | Soft scheduling for hardware[END_REF] presents an application of static analysis on scheduling hardware designs to deal with resource-sharing between hardware components. The aim is to ensure scheduling to access a shared resource throughout the hardware compilation from high-level to structural low-level languages. To achieve this, a dynamic scheduling logic is generated automatically in a manner that avoids deadlock, then the static analysis is used to remove the redundant scheduling logic which can significantly improve the efficiency of generated circuits. Another use of static analysis on HDLs is proposed in [START_REF] Athavale | Code coverage of assertions using RTL source code analysis[END_REF]. This work computes code coverage of an assertion in a given RTL source code. We note that assertions are properties that a hardware design should satisfy, and the coverage achieved during the verification is an important criterion to consider when assessing the quality of the verification results. The code coverage of the assertions is based on the coverage of the statements and their dependencies within the assertions. In order to compute the dependencies of the statements, static analysis is used to analyze the control data flow graph of the corresponding code. Finally, static analysis is also employed in the security evaluation of HDL code, as in [START_REF] Li | Sapper: a language for hardware-level security policy enforcement[END_REF][START_REF] Li | Caisson: a hardware description language for secure information flow[END_REF]. Sapper [START_REF] Li | Sapper: a language for hardware-level security policy enforcement[END_REF] and Caisson [START_REF] Li | Caisson: a hardware description language for secure information flow[END_REF] are two hardware description languages for designing security-critical hardware components. These languages express security by using static analysis at compile time. They are based on the control of the information flow to put restrictions on the information flow through the system Summary Various techniques and algorithms for program analysis have been presented in this section. We have also described their application over HDL designs for different purposes. In the following section, we present works related to the formal verification of timing properties using the model checking tool.

. Model Checking for Timing Properties

Formal verification is based on verifying properties of formal specifications, from where the necessity to generate formal models by adopting an appropriate level of abstraction. In Chapter 2, we have detailed model checking as our formal proof technique employed in our thesis as the way to verify timing properties, such as those related to the computation of WCET bounds [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF][START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF][START_REF] Metzner | Why model checking can improve WCET analysis[END_REF][START_REF] Wilhelm | Why AI + ILP is good for wcet, but MC is not, nor ILP alone[END_REF][START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF][START_REF] Touzeau | Ascertaining uncertainty for efficient exact cache analysis[END_REF][START_REF] Rieder | Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis[END_REF][START_REF] Blackham | Sequoll: A framework for model checking binaries[END_REF]. All these works employ model checking tools to explore the execution of the input program under pipeline models. Furthermore, several works have also used model checking to prove timing predictability-related properties [START_REF] Asavoae | Towards formal co-validation of hardware and software timing models of cpss[END_REF] such as the detection of timing anomalies [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF][START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF][START_REF] Binder | Is this still normal? putting definitions of timing anomalies to the test[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF], we present hereafter their applications. Various formal modeling and verification languages are used for describing models and verifying timing predictabilityrelated properties, in particular, UPPAAL in [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF][START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF][START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF], UCLID5 in [START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF][START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF] and TLA+ in [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Asavoae | Towards formal co-validation of hardware and software timing models of cpss[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF].

We start with works [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF][START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF][START_REF] Metzner | Why model checking can improve WCET analysis[END_REF][START_REF] Wilhelm | Why AI + ILP is good for wcet, but MC is not, nor ILP alone[END_REF][START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF][START_REF] Touzeau | Ascertaining uncertainty for efficient exact cache analysis[END_REF][START_REF] Rieder | Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis[END_REF][START_REF] Blackham | Sequoll: A framework for model checking binaries[END_REF] related to model checking for computing WCET bounds. The works in [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF][START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF][START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF] compute WCET bounds by using model checking for both the program and the architecture. Model checking for complete WCET estimation is first proposed in [START_REF] Metzner | Why model checking can improve WCET analysis[END_REF]. This approach is standard, both the program and the architecture (pipeline and caches) are modeled as transition systems which are then encoded in a model checker. The main point of this work is that model checking is more precise than the combination of abstract interpretation and integer linear programming (ILP), developed in the WCET analyzers. They have experimented with the behavior of instruction cache access. Thus, the model checking has proved that it provides a precise cache behavior prediction that avoids the abstraction methods' overapproximations. Since ILP is known to suffer from numerical instabilities that can produce non-valid solutions, unlike model checking, which produces correct runtime predictions. The work in [START_REF] Wilhelm | Why AI + ILP is good for wcet, but MC is not, nor ILP alone[END_REF] supports an opposite point of view, that it is preferable to estimate the WCET using this combination of abstract interpretation and ILP than model checking. The main arguments are, on one hand, the fact that model checking suffers from a state explosion problem, and on another hand, model checking cannot compute properties (e.g., invariants) as abstract interpretation. However, they are experimenting with quite complex processors. Also, according to [START_REF] Wilhelm | Why AI + ILP is good for wcet, but MC is not, nor ILP alone[END_REF], model checking may produce more precise results since it exhaustively checks all possibilities, while abstract interpretation may lose information due to abstraction.

The work in [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF] presents an approach to compute the WCET bounds based on a combination of model checking and static analysis. This work combines hardware and software components, where the hardware model consists of caching and pipelining and the software model is the control-flow graph of the application binary. Both models are represented as timed automata and model checked using the UPPAAL toolbox. Timed automata is a state machine with locations and edges. A state includes the system's variables, and the edges describe the possible transitions from the states. The main characteristics of UPPAAL is the existence of real-valued clocks in addition to finite-state transition systems. In order to evaluate the approach and to show its modularity, several implementations have been performed to support various architectures ARM7, ARM9, and ATMEL AVR. The experiments demonstrate that much tighter WCET estimates are found when taking instruction caching into account: up to 96% tighter estimates, and 72.2% on average. Also considering the data cache increases the average to 82.3%. Furthermore, the average analysis time is just under four minutes when taking both caches. Another work, in [START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF] also uses the UPPAAL toolbox to compute WCET bounds. The target architecture is a shared memory multicore system that executes parallel applications. The paper models and analyses the impact on WCET from a memory hierarchy comprising shared L2 caches and core-specific L1 instruction and data caches.

This work [START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF] considers an architecture with a 5-stage pipeline, an instruction cache, a dynamic branch prediction mechanism, a branch target buffer (BTB) and a prefetch instruction buffer. The goal is to measure the impact of dynamic branch prediction and BTB on the estimation of the WCET. The approach models both the program and the architecture using UPPAAL. The program modeling relies on slicing to narrow the set of instructions and memory locations which are useful in calculating the WCET and to limit, in this way, the state space explosion problem. The work considers a micro-architecture inspired by the e200z4 Power 32-bit architecture, a 2-issue static scheduling superscalar core with five pipeline stages. The evaluation is conducted by a set of experiments that used the Malardalen WCET benchmarks [START_REF] Gustafsson | The mälardalen WCET benchmarks: Past, present and future[END_REF] to generate the programs. The paper proves the positive impact of dynamic branch prediction modeling on the WCET estimations. Indeed, A more effective prediction strategy will result in fewer control risks and, thus, fewer configurations for the pipeline's lower stages, reducing the state space. Therefore, it shows the capacity of model checking to analyze the complex interactions between various micro-architecture components and to perform a complete analysis of the whole system.

The WCET analysis is dependent both on the properties of the program which is executed as well as the underlying hardware, thus, an accurate program and architecture analysis leads to precise WCET estimations. The architecture analysis aims to characterize the cache behavior [START_REF] Touzeau | Ascertaining uncertainty for efficient exact cache analysis[END_REF], and the program analysis requires trustworthy information about the binary code to detect unreachable code paths [START_REF] Blackham | Sequoll: A framework for model checking binaries[END_REF] and loop bounds calculation [START_REF] Rieder | Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis[END_REF]. The work in [START_REF] Touzeau | Ascertaining uncertainty for efficient exact cache analysis[END_REF] proposes an approach to remove the uncertainty in the memory access, which can lead to the over-approximation of the WCET. The approach is based on model checking to reason about unknown accesses classified with an abstract interpretation analysis.

In addition, the paper [START_REF] Blackham | Sequoll: A framework for model checking binaries[END_REF] proposes Sequoll as a framework that employs the model checking on binary code to automatically compute both simple and more complex loop bounds and verify infeasible path information. Sequoll framework derives a control flow graph from the binary. Then, this graph can be exploited to identify reducible loops defined with a single entry point from outside the loop body. Sequoll framework analyses only reducible loops via a depth-first search, locating the innermost loop for each instruction and recreating the program's loop nests. The CFG is converted into a Single State Assignment (SSA) transformation to simplify the analysis. Therefore, a program slicing is also applied to CFG with slice criteria based on the relevant variables or control flow nodes The reduced program is then exploited with model checking, which counts the number of times the loop entry node executes. Furthermore, the work in [START_REF] Rieder | Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis[END_REF] highlights also the loop bounds issues in WCET analysis. The approach includes model checking to find loop bounds for applications written in ANSI-C. The analysis framework generates some additional code to create a loop counter and to specify an assertion to be checked then with model checking. The approach was tested on several benchmarks.

We continue with works on using model checking for verifying timing predictability-related properties [START_REF] Asavoae | Towards formal co-validation of hardware and software timing models of cpss[END_REF], in particular timing anomalies [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF][START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF][START_REF] Binder | Is this still normal? putting definitions of timing anomalies to the test[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF]. Timing anomalies pose various issues in timing analysis thus this phenomenon must be defined and included in the timing analysis workflow. The work in [START_REF] Asavoae | Towards formal co-validation of hardware and software timing models of cpss[END_REF] describes an application of model checking to co-validate hardwaresoftware designs for verifying timing properties through TLA+ modeling and verification tool. The work derives the timing models from hardware and software features and verifies their consistency.

Model checking is also used to evaluate the presence/absence of timing anomalies in predictable pipelines [START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF] and study their occurrences in an industrial processor [START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF]. The automated detection of timing anomalies is implemented using bounded model checking in [START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF]. The focus of this work is on amplification timing anomalies, defined as local timing variations leading to even larger global timing variations. These timing anomalies are in general caused by memory accesses.

The formal and executable proposed pipeline models are also developed by hand, in [START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF], these models are based on a particular abstraction called the canonical pipeline model, where a pipeline stage is modeled as a single variable, and the instructions are abstracted to instructions classes. This work experiments on several predictable pipelines modeled using the UCLID5 formal framework. The amplification timing anomalies have also been verified in [START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF], which considers a processor used in the automotive field -the Tri-Core architecture. The paper extends the canonical pipeline model proposed in [START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF] to cover the dual-pipelined TriCore and considers data dependencies and structural hazards. The encoding and the verification are also performed with the UCLID5 formal verification framework.

Other works related to model checking for timing anomalies are presented in [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF]. These works focus on the code-specific problem to identify timing anomalies based on the shared resources, where multiple instructions compete for functional units. In particular, the work in [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF] considers the case of superscalar in-order pipelines, and the work in [START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF] is extended to treat outof-order pipelines. Both works use TLA+ specification language to formally model the pipelines and verify the presence/absence of counter-intuitive timing anomalies using the TLC model checker tool.

Several formal definitions of timing anomalies exist in the literature [START_REF] Lundqvist | Timing anomalies in dynamically scheduled microprocessors[END_REF][START_REF] Wenzel | Principles of timing anomalies in superscalar processors[END_REF][START_REF] Reineke | A definition and classification of timing anomalies[END_REF], which are based on the LTL logic defined in Chapter 2. The work in [START_REF] Binder | Is this still normal? putting definitions of timing anomalies to the test[END_REF] proposes a framework to test the existing definitions [START_REF] Lundqvist | Timing anomalies in dynamically scheduled microprocessors[END_REF][START_REF] Wenzel | Principles of timing anomalies in superscalar processors[END_REF]. The evaluation is performed on a formal model of an out-of-order pipeline which encodes most of the definitions of timing anomalies into an executable proce-dure based on model checking. The work in [START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF] revises the formalization of counter-intuitive timing anomalies by adding the causality concept, which establishes relations between local and global timing effects. The proposed framework applies to a concrete architecture independent of the WCET analysis method. Furthermore, the main advantage of this formalization is that it includes multiple variations and resource utilization of instructions to reason about timing anomalies executions. This evaluation framework in [START_REF] Binder | Is this still normal? putting definitions of timing anomalies to the test[END_REF] and the formalization in [START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF] are based on the TLA+ formal modeling and verification framework.

Summary. This section has presented works related to the formal verification of timing properties using model checking as the formal technique adopted in our thesis. We have described the works related to the WCET computation bounds, which employ model checking. Furthermore, we have highlighted those that focus on timing anomalies-related properties. All these works are based on building formal models of the architecture. Our work revolves around this purpose.

. Synthesis & Conclusion

This chapter reported related works relevant for our thesis work, which aims to construct micro-architecture models from hardware designs. We present next the limitations in the state of the art and the main differences that motivate the work described in the following chapters.

Many studies have been done for building pipeline models from hardware designs. Various works described come close to our approach proposed in the following chapters. We aim to generate in this thesis a dedicated pipeline model to verify timing properties. However, the works in [START_REF] Charvát | HADES: microprocessor hazard analysis via formal verification of parameterized systems[END_REF][START_REF] Mir | Modeling and verification of embedded systems using cadence smv[END_REF][START_REF] Mukherjee | Hardware verification using software analyzers[END_REF] focus on the functionality of the hardware designs given at RTL level. The construction of the pipeline models in [START_REF] Charvát | HADES: microprocessor hazard analysis via formal verification of parameterized systems[END_REF] requires preliminary information as the pipeline depth, i.e., the number of stages as in [START_REF] Kroening | Automated pipeline design[END_REF] and the architectural resources. Our objective remains mainly improved since we aim to automatically generate the datapath pipeline models by working directly on the original processor designs. Furthermore, our analysis seeks to provide a bound to the pipeline depth value.

Other works also address code-level analysis (of hardware designs) to extract pipeline models for timing analysis [3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF]. Their approach is based on abstract interpretation to create a priori correct solutions. We propose an approach that engineers a solution that could be validated a posteriori. Timing analysis on hardware designs focuses on the abstractions highlighting the timing hardware constructions, thus, our thesis work will be based on the register analysis in the pipeline models. Our approach will focus on the registers considered in the datapath part of the hardware designs. The work in [3] proposes a semi-automatic analysis that separates the control and datapath parts in its approach based on the simplification of the original design. In comparison, the work in [START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] combines program slicing with hard-coded initialization. Regarding the control path, our approach considers all the control and datapath registers as long as they are in a given set of pipeline design modules.

There are many other works [9-11, 14, 45-47] that aim to provide the required pipeline models in order to compute safe and precise WCET bounds. However, these works handcraft these models from processor manuals. They simplify the pipeline models into a single variable for a stage, which can not reflect the pipeline design (e.g., forwarding). We aim to generate datapath pipeline models with a proper abstraction level to obtain correct and precise timing analysis. We consider the pipeline mechanisms that can impact the timing behavior of the design and forwarding is among these mechanisms. The models in [9-11, 14, 45-47] are designed to prioritize the instruction progression and not its actual computation. Furthermore, certain pipeline optimizations, such as the forwarding mechanism, are not explicitly encoded in the pipeline models but are handled at the code level through arbitrary timing values. However, the work [START_REF] Kroening | Automated pipeline design[END_REF], which creates a fully functional pipeline model, also includes the forwarding mechanism in their pipeline synthesis when assigning states to stages. Finally, in [START_REF] Kroening | Automated pipeline design[END_REF][START_REF] Nurvitadhi | Automatic pipelining from transactional datapath specifications[END_REF], the correctness of the automated pipeline design is ensured during its construction while we will rely on techniques specific to software engineering to determine a solution.

The abstractions described in [3,[START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] are also based on analyzing the pipeline registers. However, these approaches analyze primarily the low-level languages Verilog and VHDL code. Whereas our thesis work will be positioned on high-level languages, we consider open-source processor designs developed with more expressive HDL languages such as Chisel/FIRRTL. Our proposed approach will work on the AST of FIRRTL, targeting the Chisel/FIRRTL compilation framework. We have presented in this chapter, through several comparatives studies [START_REF] Heilmann | Investigate the high-level hdl chisel[END_REF][START_REF] Pan | Towards gradually typed hardware description languages[END_REF][START_REF] Im | Comparative analysis between verilog and chisel in RISC-V core design and verification[END_REF][START_REF] Lennon | A comparative study of chisel for fpga design[END_REF][START_REF] Bruant | system)verilog to chisel translation for faster hardware design[END_REF] the main advantages of high-level hardware description languages called hardware construction languages, in particular Chisel language, over the low-level languages.

As introduced in this section, we have presented several techniques and algorithms for program analysis. The abstract syntax tree (AST) traversal is among these techniques described in [START_REF] Neamtiu | Understanding source code evolution using abstract syntax tree matching[END_REF][START_REF] Yang | Identifying syntactic differences between two programs[END_REF]. This AST traversal proposed in these works is similar to what we need, as we focus on registers and will also consider in the analysis the semantics of the AST nodes of the pipeline module's body. The approach in [START_REF] Yang | Identifying syntactic differences between two programs[END_REF] poses the initial assumptions as common function names between program versions to traverse and then go through the AST to determine changes. Since we are interested in a register analysis, we can fix the initial assumptions as the pipeline registers, and then we go through the AST to construct the register analysis. Other works use depen-dence graphs [START_REF] Ballance | The program dependence web: A representation supporting control, data, and demanddriven interpretation of imperative languages[END_REF][START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF][START_REF] Kim | Malware detection based on dependency graph using hybrid genetic algorithm[END_REF] to illustrate their code analysis. Our approach will construct an intermediate representation of the datapath pipeline designs. This intermediate representation performs a registers dependency graph to build the pipeline model. Furthermore, static analysis and program slicing are also presented in various works [START_REF] Clarke | Program slicing of hardware description languages[END_REF][START_REF] Bertrane | Static analysis by abstract interpretation of embedded critical software[END_REF][START_REF] Xavier Rival | Introduction to Static Analysis An Abstract Interpretation Perspective[END_REF][START_REF] Vasudevan | Improved verification of hardware designs through antecedent conditioned slicing[END_REF]. Our proposed approach for constructing pipeline models from high-level HDL designs needs also to use static analysis and program slicing techniques. Our framework provides the possibility to employ similar techniques as the program slicing. We favor the timing aspect over other functional aspects of the design. Furthermore, we also have the slicing criteria for the Chisel design as we focus on the datapath pipeline modules. We will traverse the AST only for a given number of modules: the datapath pipeline modules. In addition, we will iterate over the AST in order to determine dependency relations between registers as static analysis (fixed-point computation), which determines relations between variables. Moreover, we can verify the registers dependencies coverage as in [START_REF] Athavale | Code coverage of assertions using RTL source code analysis[END_REF], which illustrates the implementation of static analysis to cover assertions.

We have detailed in this chapter the works related to model checking used to compute WCET bounds [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF][START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF][START_REF] Metzner | Why model checking can improve WCET analysis[END_REF][START_REF] Wilhelm | Why AI + ILP is good for wcet, but MC is not, nor ILP alone[END_REF][START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF][START_REF] Touzeau | Ascertaining uncertainty for efficient exact cache analysis[END_REF][START_REF] Rieder | Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis[END_REF][START_REF] Blackham | Sequoll: A framework for model checking binaries[END_REF], also to prove timing predictability-related properties [START_REF] Asavoae | Towards formal co-validation of hardware and software timing models of cpss[END_REF] such as the detection of timing anomalies [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF][START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF][START_REF] Binder | Is this still normal? putting definitions of timing anomalies to the test[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF]. The work in [START_REF] Mangean | WCET analysis by model checking for a processor with dynamic branch prediction[END_REF] includes the branch prediction modeling in its pipeline models construction. Furthermore, [START_REF] Rieder | Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis[END_REF][START_REF] Blackham | Sequoll: A framework for model checking binaries[END_REF] computes the WCET bounds on an input program that analyzes loop bounds. In our thesis work, we aim to execute a sequence of instruction traces where the branches and bounds are already resolved for the input programs. We intend to employ model checking for the architecture as in [START_REF] Metzner | Why model checking can improve WCET analysis[END_REF] without cache behavior characterization [START_REF] Touzeau | Ascertaining uncertainty for efficient exact cache analysis[END_REF]. Instead, we will integrate the cache latencies into the input program representation to compute the precise pipeline cycles. Furthermore, we plan to use TLA+ formal modeling and verification tools based on predicate logic and suitable for the computer architecture instead of UPPAAL as in [START_REF] Dalsgaard | Metamoc: Modular execution time analysis using model checking[END_REF][START_REF] Gustavsson | Towards WCET analysis of multicore architectures using UPPAAL[END_REF].

We intend to adopt the definition of timing anomalies from [START_REF] Reineke | A definition and classification of timing anomalies[END_REF] and their integration into the existing detection procedure for timing anomalies from [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF]. The definition concerns counter-intuitive timing anomalies unlike [START_REF] Jan | Formal semantics of predictable pipelines: a comparative study[END_REF][START_REF] Binder | Scalable detection of amplification timing anomalies for the superscalar tricore architecture[END_REF] where they use model checking to verify the amplification timing anomalies with the UCLID5 formal framework. We plan to construct the pipeline models that include the pipeline mechanisms. Thus, our models differ from that of these previous works [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Asavoae | Towards formal co-validation of hardware and software timing models of cpss[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF] in the architecture modeling.

. Problem Statements

The worst-case timing analysis is performed under (micro)-architecture considerations. Our primary goal is to develop micro-architecture models, mainly pipeline models, and thus derive, in this way, the required timing models. The micro-architecture models are usually hand-crafted, frequently based on documentation [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Asavoae | Formal modeling and verification for timing predictability[END_REF] and validated through testing. There are several static timing analyzers such as the industrial-strength tool aiT [START_REF] Langenbach | Pipeline modeling for timing analysis[END_REF] and the academic ones Otawa [START_REF] Ballabriga | OTAWA: an open toolbox for adaptive WCET analysis[END_REF], Heptane [START_REF] Hardy | The heptane static worst-case execution time estimation tool[END_REF] and Chronos [START_REF] Li | Chronos: A timing analyzer for embedded software[END_REF], for which microarchitecture models are developed in such a way. Since this process is errorprone and time-consuming, we aim to address this issue through the automatic generation of these models, specifically the pipeline models. This generation should be based on open-source hardware designs and should integrate timing behavior as they are used to prove timing properties.

Recent trends in hardware design led to more processor code being made available 1 . This progress is also supported by the emergence of new, highlevel design languages (e.g., Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF] or SpinalHDL [START_REF] Papon | SpinalHDL[END_REF]), sitting at the top of specialized hardware compilation frameworks (e.g., FIRRTL [START_REF] Izraelevitz | Reusability is FIR-RTL ground: Hardware construction languages, compiler frameworks, and transformations[END_REF]). These hardware compilation chains also have the possibility to define configurable optimizations through compilation passes. In this context, the problem of deriving convenient pipeline models is backed by a comprehensive hardware compilation infrastructure. As a first purpose, we have to define the highlevel language semantics and deal with the compiler framework to develop analysis.

In order to prove timing properties, we rely on formal verification as the backbone of our work. Formal verification ensures that correct results are produced under all possible execution conditions. We focus on timing predictabilityrelated properties, more precisely on the detection of timing anomalies, thus, the need to generate formal models and then to integrate them into a procedure for the detection of timing anomalies [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF]. This application is used to demonstrate the impact of automatically generated models.

We intend to address these key elements in the following chapters.

-Workflow of Timing Models Derivation

In this chapter, we present our general workflow to address the problem of designing abstract architecture models in order to formally prove timing properties. We detail the proposed workflow in Section 4.1, followed by a description of the selected RISC-V HDL designs to illustrate our approach, in Section 4.2. In Section 4.3, we give an overview of the HDL language and its compilation framework, and then we highlight the complexity of the language semantics through several RISC-V processor designs.

. Proposed Workflow

In order to ensure the respect of timing deadlines in safety-critical realtime systems and to prove their correct behavior, we present in Figure 4.1 our general workflow for this purpose. Figure 4.1 summarizes our proposed workflow for the formal verification of timing properties related to predictability [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF], starting from hardware designs developed in a hardware compilation framework. Thus, our workflow includes four major components. We propose a workflow that analyzes the hardware designs under a compilation framework (i.e., Hardware Compiler Framework component) to extract the pipeline models for timing analysis (i.e., Pipeline Analysis and Program components). Then, these models are integrated into a model-checking toolchain for property validation (i.e., Formal Verification component). We detail next each of these components and the workflow structure from the right-hand side components to the left-hand side ones. Various tools can be used to prove the timing behavior of the system, with different degrees of confidence, from testing to formal verification. Our workflow is based on a formal verification approach. Formal verification needs to specify the system and then verify its properties. In our case, those related to timing predictability [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF]. [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF] employ a model checking on constructed formal models for this purpose.

HCL

As such, our required formal models target mainly the non-functional behavior of hardware designs, in particular the processors, as our goal is to verify their timing predictability-related properties. In other words, this means we should be reasoning about executions of an input program on an underlying architecture. In this setting, both aspects, that of the program (software) and the architecture features (hardware), become equally important to characterize the timing behavior of the system. The program provides a sequence of instructions to be executed while the architecture adds timing to this sequence, e.g., counting clock cycles while instructions pass through the pipeline stages. Since we do not need to consider all the functional aspects in our pipeline models, the proposed formal models are based on an abstraction that considers the execution progress of the instructions from the program through the pipeline with cycle-accurate granularity. This combines the Program component and Pipeline Analysis component. Therefore, the abstraction focuses on the sequential logic of the pipeline, more specific details are addressed in Chapter 5.

A pipeline design includes a datapath and a control path. Automatic construction of these architectural models is possible because hardware designs are made available, i.e., open-source, and are supported by the emergence of high-level Hardware Description Languages (HDLs) and hardware compilation frameworks, for example [START_REF] Bachrach | Chisel: constructing hardware in a scala embedded language[END_REF][START_REF] Papon | SpinalHDL[END_REF][START_REF] Schuiki | LLHD: a multi-level intermediate representation for hardware description languages[END_REF]. Different ways to abstract the pipeline can be derived while analyzing its code, both data and control paths. Chapter 3 gives more details on the abstract models constructed. In our workflow from Figure 4.1, the pipeline datapath model is automatically constructed. We note that the control path captures the instruction flow through the pipeline stages and currently, the control flow is manually developed and integrated with the datapath in our model. Then, we also need to map the instructions, i.e., the input program, on the abstract pipeline models such that we could define an execution model, in terms of both software and hardware aspects.

Generating formal models from hardware designs is based on the accurate representation of specific details of the processor micro-architecture. In our workflow, in particular the Hardware Compiler Framework component, they are derived from HDL processor designs, presented in Chapter 2. We are interested in high-level design languages that pose different challenges when generating abstract processor models specific to the targeted properties. We specify the main challenges in Section 4.3. Note that our contribution related to the automatic generation of abstract processor models is agnostic to the choice of a hardware compilation toolchain but it is presented for Chisel/-FIRRTL workflow. More precisely, we propose an analysis of HCL processor designs based on the high-level language Chisel [START_REF] Bachrach | Chisel: Constructing hardware in a scala embedded language[END_REF], sitting at the top of spe-cialized hardware compilation frameworks (e.g., FIRRTL [START_REF] Izraelevitz | Reusability is firrtl ground: Hardware construction languages, compiler frameworks, and transformations[END_REF] ). These hardware compilation chains also have the possibility to define configurable optimizations through compilation passes. So, how can we take advantage of hardware compilation frameworks to ease the generation of abstract pipelinelevel models? In this context, the problem of deriving convenient pipeline models is backed by a comprehensive hardware compilation infrastructure.

The HCL designs and their intermediate representations (IR) generated with the compilation chains correspond to the input of our workflow. The Chisel/FIRRTL compilation chain is described in detail in the next section 4.2. Our proposed approach to generate automatically the abstract pipeline models is described in Chapters 5 and 6. Then, we highlight the formal model generation from the abstract pipeline models, this constitutes the output of our workflow. Finally, we present the use of such outputs for the verification of timing predictability-related properties. Both, workflow output generation and its application are detailed in Chapter 7.

. Chisel/FIRRTL High-Level HDL Designs

We select the Chisel/FIRRTL hardware-compilation toolchain [START_REF] Bachrach | Chisel: constructing hardware in a scala embedded language[END_REF][START_REF] Izraelevitz | Reusability is firrtl ground: Hardware construction languages, compiler frameworks, and transformations[END_REF] to illustrate our approach. Chisel (Constructing Hardware In a Scala Embedded Language) [START_REF] Bachrach | Chisel: constructing hardware in a scala embedded language[END_REF] is an open-source hardware-construction Domain-Specific Language (DSL) embedded in the Scala programming language. Chapter 2 introduced the Chisel language and its corresponding Chisel/FIRRTL hardware compilation framework. Chisel constitutes the frontend part of the toolchain, FIRRTL is the middle-end from which all Scala-related hardware generators have been executed, and Verilog is the backend. We focus next on describing the Chisel language and the FIRRTL representation, highlighting the main features needed to develop our analysis.

. Chisel Hardware Description Language

Chisel offers a set of Scala libraries to write complex, parameterizable circuit generators and new hardware types that can be manipulated to produce synthesizable Verilog. Each constructor in Chisel language combines the hardware design elements and software programming features provided in Scala language.

We introduce in this section some features of Chisel (Hardware Compiler Framework component) with applications in RISC-V processor designs. These examples include both Chisel (Module, Reg, Wire, Bundle, Vec, etc.) and Scala constructions (val, class, function, etc.). Our pipeline analysis is grounded on these constructs, hence on these languages and the compilation toolchain. Chapters 5, and 6 address this pipeline analysis.

Modules.

A hardware design in Chisel would typically consist of a set of modules. Chisel modules are defined using Scala classes, i.e., the keyword class. A Chisel module contains at least one interface wrapped in an object IO(). For example, a Chisel DatPath module of the RISC-V Sodor processor [1] The variable if_pc_next is a wire declared inside the module DatPath and assigned later with the value if_reg_pc + 4, where if_reg_pc is a register initialized to io.reset_vector, line 12, while d is an instance of DatPath defined in Scala language with new in the module Core, in lines 14-19, which is further used to access and update this particular value. The remaining constructions are described later. The operator <> is used to connect two modules, Rocket and IBuf, in Listing 4.4, line 3. Furthermore, the when block is used to perform a conditional register update, whenever the condition evaluates to true.

Ports

. FIRRTL -The Intermediate Representation

FIRRTL language also has first-class support for high-level constructs such as vector types, bundle types, conditional statements, partial connects, and modules. These high-level constructs are then gradually removed by a sequence of lowering transformations. Eventually, the circuit is simplified to resemble a structured netlist, which can then be translated into any output language (e.g., Verilog). All FIRRTL constructs interoperate with one another; a simplified circuit is expressed using a subset of the FIRRTL specification.

The FIRRTL representation is internally represented with an Abstract Syntax Tree (AST) structure as described in Figure 4.2, where passes recursively visit nested elements to manipulate the AST. Chapter 2 presents an example of this pass. It consists of IR nodes represented by objects, each of which is a subclass of the following IR abstract classes: circuit, module, port, statement, expression, or type. The circuit is the root node of any FIRRTL data infrastructure, it consists of a set of modules. The statement node describes the module body and includes the combinatorial and sequential logics as registers, connections, conditional blocks, etc. Each register update is represented by a connect node that is also part of the statement class. Expressions represent references to declared components or logical and arithmetic operations.

Like the software compilers, the FIRRTL compiler framework transforms the designs to the RTL level. It enables this automatic design transformation through optimizations and other generic passes. Thus, the main features of FIRRTL-based hardware compilation are its reusability and its extensibility of customization. As such, we can develop and integrate custom passes in this toolchain at different levels. Then, the compiler supports a robust mechanism for communicating information throughout the compilation process to the lower level. In this context, a question would be to find what are the main differences between the FIRRTL levels, and which level is the most appropriate to integrate our custom analyses via compilation passes. More details are addressed in the next section.

. Pipeline Construction in the Chisel/FIRRTL Framework

We describe in this section a description of the compilation framework issues and features in Sections 4.3.1, and 4.3.2, followed by the presentation of Chisel-based RISC-V processor designs for the goal of reporting the semantics language complexity in Section 4.3.3.

. Choice of FIRRTL Forms

FIRRTL proposes different Intermediate Representations (IRs), named forms (i.e., high, mid, low). Each form uses a smaller, stricter and simpler subset of the Chisel language features and defines different transformations to generate the next (lower) form. Compiling FIRRTL to Verilog is developed as a set of passes that implement optimizations, such as constant folding or dead-code elimination. A so-called high form supports the Chisel high-level constructs such as vector types, bundle types, and conditional statements that must be lowered for synthesis. These constructs are replaced by a set of low-level features, resembling a structured netlist that simplifies its translation to Verilog, in the form named low-form. mid-form and low-form, are increasingly restrictive subsets of the FIRRTL language that omit many of the higher level constructs.

We now describe the differences between the high and low forms, through several cases results from FIRRTL compilation. We also highlight some compilation issues from Chisel to FIRRTL representation.

High/Low forms: Conditional Statements. The high form supports highlevel constructs such as conditional statements as when conditions, while in the low form, these kind of statements go through multiple optimizations producing instead a simplified and flattened set of multiplexers. The aim is to be closer to hardware representation, as translated into Verilog.

We illustrate now this case, through a very simple example presented by Listing 4.5. This example defines two registers, reg1 and reg2, at lines 1 and 2.

Both registers are initialized on reset using the RegInit construct. Note that the reset and clock signals are implicit in Chisel (but can be explicit in the FIR-RTL forms). Finally, both registers are updated at lines 3 and 4, but for register reg2, this update depends on the value of the cond variable (actual value not defined to simplify) and is thus performed within a Chisel when construct (line 4). It can be noticed that the when statement remains in the high form (line 6, Listing 4.6), while it is translated into a multiplexer in the low form (line 5, Listing 4.7). Note that in Chisel, a condition can be translated into a set of multiplexers to implement a multi-variable condition.

Such a statement can be safely translated into a formal statement when targeting a pipeline-stage abstract model. Thus, the higher-level form facilitates the integration of our design-level properties, which demonstrates the need to develop custom FIRRTL passes in high-level form.

. Chisel to FIRRTL Compilation Issues

Chisel is compiled in FIRRTL representation through multiple passes. Our analysis is positioned in FIRRTL high-level form. We present next the main issues and differences through the compilation from Chisel constructions to FIRRTL high form.

RegNext Construct Compilation. The register update can be expressed in Chisel in different ways, as explained in Section 4.

The Chisel construction

RegNext is employed in order to delay one cycle the associated register update. In order to ensure this delay through compilation, an additional register is implemented for each delay at the FIRRTL high-level form.

We illustrate now this implementation through an example in the Kyo-genRV processor described in Listing 4.8. The registers imem_read_sig, imem_req are two Boolean registers, where the second one is updated under the conditional statement when with RegNext construction with the value of the first register respectively (line 4). We notice that at the FIRRTL high-level form in Listing 4.9, an additional register REG_1 appears in conditional block when, lines 6-8. It ensures the one-cycle delay for the register imem_req update. Generally, these additional registers are identified by a general structure REG in our analysis. This issue can produce an additional register dependence, which leads to an inaccurate analysis. However, we can handle this issue by relying on these registers FIRRTL names. connected then in high form FIRRTL level. The interfaces between modules are implemented using this kind of connection components. Thus, their compilation into FIRRTL high form level leads to connecting the constructions of the modules interfaced. However, it can add a cost in terms of analysis runtime.

. Description of Chisel-Based Processor Pipelines

The pipeline architecture in Chisel-based processors also includes a control path and datapath. Using the modularity of Chisel/Scala, Chisel hardware designers can develop the control path and datapath in separate modules that interact with each other. As such, it facilitates the management of the abstract pipeline models expected to generate, with a clear overview of the pipeline design. Furthermore, we can analyze both control and datapath with the aim of generating timing models without focusing on the functional aspect. We introduce next several hardware design features using code snapshots of RISC-V processors designed through the Chisel/FIRRTL compilation framework. We intend to describe how the pipeline architecture is built in Chisel-based processors. We detail the pipeline structure in Chisel, the connection between pipeline stages through the connection between pipeline registers, and how the micro-architecture mechanisms such as forwarding are implemented in Chisel.

We present first the pipeline design structure of different Chisel-based processors. We exemplify them with the mono-module pipeline of KyogenRV processor [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF], then the multi-module and hierarchical pipeline design of the Rocket processor [2] and the flat and parametric pipeline construction of the Fuxi processor [START_REF]Fuxi, a 32-bit pipelined risc-v processor written in chisel3[END_REF]. The multi-module pipeline refers to the pipeline design specified in several FIRRTL modules. We present how Scala constructions added in Chisel implement the connection between these modules. Finally, we present two different implementations of the forwarding mechanism, as developed in RISC-V Sodor [1] and Fuxi [START_REF]Fuxi, a 32-bit pipelined risc-v processor written in chisel3[END_REF] processors. Listing 4.12 describes a simplified Chisel pipeline code of the KyogenRV processor. The pipeline datapath is specified in a single Chisel module named KyogenRVCpu. The pipeline registers are all defined inside this module, lines 2-5. The sequential logic represented by registers is updated through the combinatorial logic using when conditional block, lines 6-8. Thereafter, the connection between pipeline stages is established. Listing 4.12 -Simplified Chisel code of Kyogen datapath pipeline. module RocketTile: inst frontend of Frontend inst core of Rocket core.io.imem.resp.bits.pc <= frontend.io.cpu.resp.bits.pc --------------module Rocket: inst ibuf of IBuf when cond1 : ex_reg_pc <=ibuf.io.pc Listing 4.13 describes how the pipeline modules are connected. Thus, we illustrate the connection between the registers PC (i.e., those with _pc suffix) of all the pipeline modules in different stages. The RocketTile module is designed to connect the modules Frontend (not shown) and Rocket, in line 2 using their respective IO interface (frontend.module.io.cpu <> core.io.imem), in line 3. This connection is shown with red arrows in Figure 4.4 and implemented using the bulk operator <> in Chisel. The PC registers ex_reg_pc, mem_reg_pc, wb_reg_pc are described in the same module, i.e., Rocket, while the PC register of the decode stage is presented in the IBuf module. IBuf is instantiated in Rocket in order to connect the decode and execute stages through the output io.pc, which receives the output of the register buf.pc in the IBuf module, in lines 28-30 in Listing 4.7.

KyogenRV

The registers of fetch and decode stages are connected through the interfaces between the corresponding modules. The register buf.pc of the decode stage, in the IBuf module, is interfaced with the input port io.imem.bits.pc, in line 27 in Listing 4.7. The PC registers s1_pc and s2_pc of the fetch stage are in the Frontend module, and s2_pc is connected to the output port fq.io.enq.bits.pc which is an element of the ShiftQueue module, in line 21 in Listing 4.7. Here, the ShiftQueue module is used as an I/O interface as it connects the input io.enq to io.deq which is connected to the output io.cpu.resp. Thus, the fetch stage register s2_pc is connected to the output io.cpu.resp, while the input io.imem.bits.pc is connected to the decode stage register buf.pc. Finally, the connections between registers in pipeline stages are obtained through the IO interface of the module RocketTile.

Fuxi Pipeline. Fuxi is a 32-bit pipelined RISC-V processor, designed to run simple operating systems and bare-metal software. In contrast to the hierarchical pipeline design of Rocket, in Fig. 4.4, the pipeline design of Fuxi is flattened, in Fig. 4 The forwarding of Fuxi is implemented using a Scala function forwardReg with IO interfaces as parameters, i.e., the register file rf and the operand read, as shown in Listing 4.17, line 1. Fuxi proposes an alternative implementation of the forwarding condition checks C1-C3, namely the MuxCase implementation of Sodor is replaced by when-.elsewhen statements of Chisel, in lines 3-10. Each forwarding path is then created using calls to forwardReg, in lines 13-14. This function is called for two operands of the instruction in the Decode stage: io.regRead2/io.regRead1. Thus, the data read.data is updated under the when condition if it matches execute, memory, or write back addresses.

At the FIRRTL level, the hardware compilation framework flattens all the abstract functions and takes into account the function calls with the call parameters instead. The Listing 4.18 describes the corresponding FIRRTL high form of the function forwardReg(io.regRead1, io.rf1) called in Listing 4.17, line 13.

Listing 4.17 -Forwarding implementation in the pipeline of Fuxi. The code snippets in Listing 4.13 to Listing 4.18 present processor design choices addressed using Scala/Chisel programming language-specific constructs. Since Chisel is built over Scala, it is often the case that processor designs mix constructs of the two languages. For example, the forwarding of Sodor combines a Chisel MuxCase with a Scala Array, while the forwarding of Fuxi embeds a Chisel when-.elsewhen in a Scala function. Furthermore, all the connection between pipeline modules is performed using the interface IO. They are implemented in Chisel with the bulk connection construct.

Different descriptions of Chisel-based processors are presented in this section, such as the pipeline structure and the various ways to implement the forwarding mechanism at Chisel and its compilation at the FIRRTL level. We have shown that relying on the FIRRTL level allows us to capture the Chisel diversity in our analysis. Furthermore, we highlight the complexity of the hardware compilation framework to compile the Chisel constructions.

. Conclusion

In this chapter, we have detailed our proposed workflow, which is to be used to formally prove timing properties. We have proceeded first to present the selected high-level HDL language and its compilation framework Chisel/-FIRRTL, as the expected input of our workflow. We have introduced then the Chisel constructions that we rely on to develop our approach in Section 4.2. The main goal of Chisel HDL is to allow complex hardware designs from simple components using an advanced module system (in a combination of Scala's features and Chisel's specialized operators and language constructs). In essence, Chisel proposes syntactic sugars to represent a hardware design as a series of primary component updates (wires, registers) under various static and dynamic evaluation contexts (classes, objects, functions, when-blocks etc.). Chisel is compiled in FIRRTL representation which has three levels (high, mid, low), and designs written in Scala are typically transformed into the high form of FIRRTL, which goes through multiple optimizations passes to a low form. Since we aim to formally verify the timing properties, we need to construct the micro-architecture models with an appropriate level of abstraction. Thus, we implement our analysis at the high form of FIRRTL, where the designs are not flattened and preserves the Chisel semantics as when conditional blocks (that FIRRTL low form flattens their structure and uses a Mux instead, making the condition extraction more difficult). These Chisel statements describe the different execution paths under conditions that go with timing properties analysis.

The complexity of the hardware compilation framework and the diversity of Chisel design implementations presented in section 4.3 confirm the need for studies of the hardware compilation features/issues. Furthermore, the code analysis of Chisel HDL processor designs (e.g., pipeline structure -stages, register forwarding, etc.) is the first brick in our approach. Therefore, the abstract pipeline model needs to include the pipeline structure in terms of single/multi-module pipeline, also the hierarchy of the pipeline in order to ensure the efficiency and strength coverage of our approach.

We intend to address our approach that generates the abstract pipeline models in the next Chapters 5, and 6.

-Register Analysis of Pipeline Designs

The construction of the complete abstract pipeline models requires both datapath and control path models as described in the workflow in Figure 4.1. Generally, these pipeline models are developed manually and their development is based on the manuals provided by the manufacturers of the hardware platforms. However, in our work, we aim to automatize the construction of abstract datapath pipeline models combined with manual control logic to define the execution models on these architectures.

Each datapath pipeline design comprises several components (ALU, CSR, Memory, Registers, etc.) that perform all the required operations. Since our approach aims to verify the timing properties, we construct the abstract datapath models with a focus on the timing aspect of the pipeline; namely, we focus on the pipeline stages and, more precisely, the pipeline registers.

In this chapter, we describe how we can construct datapath pipeline models automatically, starting with a register analysis. We present the registers analysis for different pipeline structures in Section 5.1. We apply this analysis on RISC-V Chisel-based processors and detail the results in Section 5.2. Then, we summarize the experimental results on these RISC-V processors in Section 5.3.

. Register Analysis Formalization

In order to construct a pipeline datapath model for the timing analysis, we need to determine the pipeline depth (i.e., the number of pipeline stages) as well as the connections between these stages. A pipeline stage is to be identified by a set of registers, which are updated whenever the pipelined execution passes from a stage to another.

Intuitively, the construction of a pipeline datapath proceeds as follows: we compile the Chisel code of hardware designs into the corresponding FIRRTL representation (AST). Then, we proceed with the development of our custom pass, which allows us to process the FIRRTL AST and build the desired datapath pipeline abstraction. Writing a FIRRTL pass usually requires writing functions that traverse the FIRRTL data structure (AST) to either collect information or replace IR (i.e., Intermediate Representation) nodes with new IR nodes. The circuit is the root node of any FIRRTL AST, and there is only one Circuit. The circuit contains a list of module definitions and the name of the top-level module. The pipeline modules are given as input, and for each register in these modules, we investigate each module in order to perform a register analysis to determine precedence relations between registers. We also perform an output port analysis to determine how registers from different modules will be connected. Finally, we provide an assignment procedure to map each register to a pipeline stage according to the results of the previously mentioned analyses. This phase is more detailed in the next Chapter 6. Next, we introduce some notations and definitions, following a standard set-theoretic approach.

Notations. We consider Pr = {M 1 , M 2 , ..., M n }, a processor design, defined by a set of n modules M i and P the pipeline of Pr, with P ⊆ Pr. We assume that P is given and the (FIRRTL) AST of P is denoted by AST P , so as AST M represents the AST of each M ∈ P.

Furthermore, for each module M ∈ P we define: -Insts, the set of instanced modules, -I/Os, the set of input/output ports, -Regs, the set of registers (or sequential logic), -Combs, the set of combinatorial elements (e.g., wires, multiplexers, etc.), -Ctxs, the set of contexts (scopes), -Exts, the set of external entities. Each of these sets, when subscripted by M represents the corresponding set of a module M and, when subscripted by P, represents the union of all the corresponding sets of the pipeline modules in P.

An element ins ∈ Insts M identifies the name and the type of a module instantiated in M . The module of P which contains directly or indirectly (through transitivity) the instances of all the other pipeline modules in P is called 'top', denoted by ⊤.

Furthermore, an element x ∈ I/Os, Regs or Combs is the identifier of the respective design element, i.e., x is a name of an input/output port or a register or a wire.

An element ctx ∈ Ctxs M is defined as a mapping between the context condition and the respective register updates in M . A context, which is expressed in Chisel with a when statement, allows guarded register updates (or any other combinational element) in a compact manner. Moreover, when is often used to provide alternative updates of the same register, updates which are guarded by different conditions.

Our approach considers a given set of pipeline modules P, which is a subset of Pr, the complete processor design.

We denote by Exts, the set of all design elements (i.e., ports, registers, wires, etc.) which are defined in Pr \ P. For a module M ∈ P, we define by Exts M , the set of external design elements which are used in M . For example, Regs M consists of only the registers defined in module M , whereas the "external" registers of M (e.g., defined in other modules but used in M ) are to be included in Exts M . A similar argumentation stands for I/Os M and Combs M with ports and respectively, wires being also included in Exts M .

. Register Analysis Algorithm

We present next the algorithm to construct pipeline datapath models from Chisel-based processor designs. As such, we introduce an intermediate representation of the processor pipeline P, based on the set of pipeline registers Regs, a set of dependency relations between these registers, and a set of contexts Ctxs. The dependencies between registers are used to produce chains of registers, and the contexts are used to determine additional relations between these registers, encoding how the processor is coded. Intuitively, this intermediate representation is a non-strongly connected graph with registers as nodes and their dependencies as edges. Also, different contexts determine different connected components in this graph.

The sets Regs, Combs, I/Os and Ctxs of P are obtained, for each module M ∈ P, from the AST P , using the standard visitor from [START_REF] Izraelevitz | Reusability is FIR-RTL ground: Hardware construction languages, compiler frameworks, and transformations[END_REF]. We name this operator process_mod : AST M → I/Os × Regs × Ctxs.

The initial partition of the processor design Pr into the pipeline design P is also sufficient to determine the set Exts.

The following Algorithm 1 illustrates our AST visitor used to construct the sets Regs, Combs, I/Os and Ctxs of P. Algorithm 1 is a recursive algorithm that visits all FIRRT nodes in the AST. First, we start with the root node circuit of our FIRRTL AST, line 2. The circuit is composed of a set of modules. We visit each module with the function walkModule, lines 5-7. For each visited module, we visit the module body which includes the set of statements and ports through walkStatement, lines 9-15 and walkPort functions, lines 17-20. The statement node contains the registers defined as DefRegister node, conditions through Conditionally node, updates and assignment of variables as Connect node, etc., lines 12-14. Moreover, the ports can be an input or an output module defined as BundleType node with a specification of the direction, line 19. We store the set of registers, contexts, and input/output ports from the nodes browsed. For each visited statement, we visit each of its children statement and expression nodes expressed in walkExpression function, lines 22-25. Note that all the FIRRTL transformations use these recursive walks of the FIRRTL AST to modify or simplify the circuit.

To express a recursive walk, every IR node has implemented a custom map function. A node's map applies a user-specified function to the subset of children whose node type matches the function's input and return node type. For example, in walkModule function, map function will be applied to the module's children which are the statement nodes, and then return the module as the node type, lines 6-7. We recursively walk all FIRRTL modules, statements and expressions by calling map on modules, statements and expressions. This procedure is called the pre-order traversal, as we traverse the FIRRTL AST using map to write recursive functions that visit every child of every node.

Algorithm A depth-first search traversal of the AST P establishes an order between the considered pipeline modules, determined by the instancing relation, i.e., the set Insts. However, for a module that is instantiated several times, e.g., MidStage of Fuxi, in Listing 4.15, our approach computes a module summary and uses it for all instances of this particular module. We denote by order_mods : P × AST P → P an operator which establishes an order between the pipeline modules up to top ⊤ as the last element.

Informally, an analysis for a module has (1) an intra-module component that focuses on the module's registers and (2) an inter-module component that overcomes the module and focuses on the module's interface (i.e., inputoutput ports), in order to connect between several pipeline modules.

We address the intra-module part by computing dependencies between registers through a visitor combinator, characterizing the connectivity of each register w.r.t. the other design elements. Operationally, for a given register r in module M , a visitor combinator iteratively collects the nodes of the AST M which affect the inputs of r. This iterative process corresponds to a standard dataflow analysis which terminates at a register frontier, defined next.

Definition 12

For a register r ∈ Regs M , we denote by In r the input frontier of r, defined by {c 1 , c 2 , ..c i .., c n }, where

c i ∈ Regs M or c i ∈ I/Os M or c i ∈ Exts M .
Such an input frontier contains three kinds of design elements: registers (i.e., that precede r in the pipeline datapath), ports or other design elements of the considered pipeline P. These are stop conditions of the visitor combinator as it aims to collect, for all registers in each module M ∈ P, the respective register contexts. The goal of the inter-module part of our analysis is to determine, for each pipeline module an input-output interface in order to connect the registers of different modules. Hence, we also define an output frontier of a module. For a pipeline module M , for all registers r ∈ Regs M and output ports p ∈ I/Os M , the operators regs_ctx and ios_ctx determine a summary of M .

Next, our approach determines the dependency relations between registers. We establish first a precedence relation between two registers then we use these relations to define our working structure.

Definition 16

For two register contexts C r1 and C r2 of r1 and r2 respectively, a predicate prec(r1, r2) is true if r1 ∈ In r2 , i.e., in the input frontier of r2, and false otherwise. We denote by P red the set of (r1, r2) with r1, r2 ∈ Regs, for which prec(r1, r2) evaluates to true.

Definition 17

The intermediate representation of a pipeline design P, denoted by IR P is a non-strongly connected graph G = (V, E) with the set of nodes V = Regs and the set of edges E = P red.

. Application to RISC-V Processors

We present the register analysis application for various RISC-V Chisel-based processors. Section 5.2.1 details the mono-module datapath pipeline application. Then, we continue with the multi-module designs illustration in Section 5.2.2.

. Mono-module Datapath Pipeline Design

The mono-module datapath pipeline design refers to the datapath pipeline specified in a single FIRRTL AST module. Figure 5.1 illustrates the mono-module design with a focus on the main Chisel/FIRRTL construction of register analysis. All the analyses for a mono-module pipeline are performed in the relevant module and delimited by the module interface I/O. For each register in the pipeline module, we construct the register context with a recursive walk through the combinatorial logic until the input frontier as a stop condition. These combinatorial logics present the operations such as those with a single operand op1 as NOT, and with two operands as operations Mux, AND, XOR, OR etc. We Now, we illustrate the Algorithm 1 application on the RISC-V Mini processor in Figure 5.5. RISC-V Mini processor is mono-module datapath pipeline design; its datapath pipeline is specified on a single module named Datapath. Through process_mod function, we process this module to get the ports that are stored in DatapathIO IO module and the module body which is a set of statements. In order to construct the context registers, for each register, we walk through the statements until input frontiers, which are expression nodes in FIRRTL AST. For example, to construct the context of the register

. Multi-module Datapath Pipeline Design

The architecture of the pipeline design is becoming increasingly complex. This complexity can be characterized in pipeline structure for example. As described above, the datapath pipeline design can be a mono-module or multimodule architecture. The multi-module datapath pipeline designates the datapath pipeline developed in several FIRRTL modules. Each module describes single or multiple pipeline stages. Then, the connection between modules is obtained through the interface IO. Adding to the intra-module register analysis on each module, we extend the approach to the inter-module analysis. The connection between registers in a multi-module datapath pipeline design requires constructing the output context delimited by the output frontier. This context enables then the possibility to connect registers of different modules.

Example 9

The output context of io.cpu.resp.bits.inst and io.cpu.resp .bits.pc in FrontEnd module, as the pairs <exe_reg_pc, io.cpu.resp.bits.pc> and <exe_reg_inst, io.cpu.resp.bits.inst>, in Listing 5.2, lines 47-48. They include the registers exe_reg_inst, exe_reg_pc as their output frontiers. 5.9) is derived for all the datapath pipeline design.

. Experimental Results

We implemented our approach in Scala as a pass in the Chisel/FIRRTL hardware compiler framework. We evaluated its results on several opensource Chisel-based RISC-V processors described in detail in Section 2.2.2. Each processor design is considered as is, without manual modifications or and 16GB RAM memory. We consider the following six RISC-V processor designs: RISC-V Mini [START_REF]Risc-v mini[END_REF], Sodor [1] with 3-stage and 5-stage, KyogenRV [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF], Fuxi [START_REF]Fuxi, a 32-bit pipelined risc-v processor written in chisel3[END_REF], and Rocket Chip [2]. These processors are developed in different Chisel versions, from '3.2' for Fuxi to '3.5' for Rocket. Our analysis is applied over single and multi-module datapath pipelines and these processors include both structures. We report the results of our register analysis in Table 5.1. We summarize the processor statistics related to the code and the pass results. The first three lines in Table 5.1 report the processors made of a single module implementation of the pipeline datapath, while the three last lines concern the multi-module pipelines.

The first column, LOC presents the code size of each pipeline P, while the second column, #M P indicates the number of pipeline modules single or multi-module, i.e., the cardinal number of P. The following three columns report statistics related to the numbers of registers #Regs, of contexts #Cxts as well as the largest input frontier #F rt. This parameter measures the maximal connectivity between a register and other design elements, either sequential or combinational. Then, the next column #IR P summarizes the intermediate representation results. It reports the resultant graph depth, i.e., the cardinal number of P red. Finally, the last column reports the run time of the register analysis algorithm 2.

We can notice that the run-time of register analysis refers mainly on FIR-RTL AST recursive traversal (#IR P construction is not significant). This runtime value increases with the number of modules and depends on the datapath pipeline structure. For example, it is longest for the Fuxi processor, where the datapath pipeline is developed in 10 modules, and the pipeline structure is a linear traverse across the width of the pipeline. This leads to frequent module changes moving between pipeline stage modules and the MidStage module, as illustrated in Figure 4.5 in Section 4.3.3. Furthermore, the size of the intermediate representation graph is proportional to the number of registers for all the processor designs. The graph for Rocket processor is the largest, a 5-stage multi-module datapath pipeline design composed of 240 registers, and this graph is smallest for RISC-V Mini, a single 3-stage pipeline design.

. Conclusion

We have presented our approach that automatically generates the abstract datapath pipeline models, starting with the first phase: the register analysis. We have described the main steps to develop this register analysis by developing different algorithms working directly on the hardware designs at the FIRRTL level.

Our goal is to generate an intermediate representation of the datapath pipeline designs. In our case, it is represented as a non-strongly connected graph. The nodes are datapath pipeline registers, and the edges correspond to the dependency relation between registers and registers with the same context. We have applied this analysis to various RISC-V Chisel-based processors with different pipeline depths, and we summarized the processor illustrations and their experimental results.

The resultant intermediate representation will be the input feature for the following phase in our approach, where we assign pipeline registers to their respective pipeline stage. We present this phase next, in Chapter 6.

-Automatic Generation of Abstract Datapath Pipeline Models

The automatic generation of abstract pipeline models requires information about how the pipeline is designed, for example, if it is coded as a single or a multi-module pipeline (i.e., Chisel modules) and also if there is a hierarchy of modules. In Chapter 5, we have presented the first phase of our approach, which outputs an intermediate representation of pipeline datapath based on a register analysis. We intend to address in this chapter the second phase, which is built around two objectives: to determine the pipeline depth defined by pipeline stages and to identify how to connect these stages.

We detail in this chapter the automatic construction of the abstract datapath pipeline model, presenting the procedure to assign registers to pipeline stages in Section 6.1. Then, we exemplify our approach on several opensource RISC-V processors (in Section 4.3.3) of various degrees of complexity, i.e., from single to multi-modular pipeline designs, with the application being described in Section 6.2. In Section 6.3, we report on the experimental results.

. Construction of Abstract Datapath Pipeline Models

The automatic generation of abstract datapath pipeline models is based on two phases. The first phase is based on register analysis, which outputs an intermediate representation of the pipeline design described as a nonconnected graph. The second phase relies on a register-to-pipeline stage assignment function to determine the datapath model. This phase provides an assignment procedure to map each register to its corresponding pipeline stage according to the results of the previously mentioned analyses. Next, we introduce some notations and algorithms of the assignment procedure.

Algorithm 3 summarizes the two phases of the construction algorithm of the datapath pipeline. The first phase corresponds to the register analysis presented in the previous Chapter and described in lines 1-6 in Algorithm 3.

The second phase of the registers' assignment is described in the assign_regs function.

The abstract pipeline datapath of pipeline denoted by P is constructed by unfolding its intermediate representation IR P and assigning nodes (i.e., registers) to pipeline stages. We denote by to_stage : Regs → N + an operator to assign to the registers their stages. present a cycle and nodes that correspond to the registers that can not all be connected. Thus, this algorithm starts by assuming that the program counter P C ∈ Regs, assigned in the first pipeline stage, i.e., to_stage(PC) = 1, and performs two assignment strategies.

We distinguish two cases: case 1 driven by register dependencies and case 2 driven by a heuristic defined using the context dependencies, Ctxs. We further define three possibilities for case 1 : the linear_case 1 , the min_case 1 and the max_case 1 . When the selected register r cannot be assigned by the above conditions, the operator select_reg selects another assigned register r ′ to stage i ′ from which we proceed, in line 16.

Linear_case 1 (lines 2-4 of Algorithm 4) is applied when the register has only one source. More specifically, a register r is assigned to the pipeline stage i + 1 if it is the only destination register of reg, which is already assigned to stage i. Formally, it is applied when the condition C1_linear is true, where

C1_linear = ∃!(reg, r) ∈ P red
Min_case 1 (lines 5-7 of Algorithm 4) considers the case when several source registers are already assigned with no precedence relation between the source register of the minimal stage and the other source registers. The stage assigned to r strictly follows this minimal stage of its source registers, which are already assigned to later pipeline stages. Thus, they are connected to r through backward edges (i.e., the forwarding mechanism). This case is applied to some configurations of the forwarding mechanism.

Formally, the min_case 1 is applied to assign r, preceded by regs, when the condition C1_min is true, where Max_case 1 (lines 8-10 of Algorithm 4) also addresses the case of several source registers that are already assigned. It checks if the source register of the minimal stage is directly connected to all the other sources. In that case, the stage assigned to r follows the maximal stage of its source registers.

C1_min = ∃(reg, r) ∈ P red ∧ to_stage(reg) = i ∧ ∀(r 2 , r) ∈ P red, r 2 ̸ = reg ∧ to_stage(r 2 ) >= to_stage(reg) ∧ ∄(reg, r 2 ) ∈ P red
Formally, the max_case 1 assigns r (preceded by reg) when C1_max is true, where

C1_max = ∃(r 2 , r) ∈ P red ∧ to_stage(r 2 ) = i + 1 ∧ ∀(reg, r) ∈ P red ∧ r 2 ̸ = reg ∧ to_stage(r 2 ) >= to_stage(reg) ∧ ∃(reg, r 2 ) ∈ P red Figure 6
.2 illustrates this case, which is found in the Rocket processor to consider compressed instructions in the pipeline design. We explain this implementation later. The two source registers buf.pc and s2_pc of register ex_reg_pc are already assigned, and moreover, s2_pc precedes buf.pc. So, we assign to register ex_reg_pc the maximal stage (i.e., that of buf_pc plus 1). Rocket is able to handle compressed instructions. Thus, the pipeline design has an additional stage to accommodate them, becoming a 6-stage pipeline instead of a 5-stage one. Listing 6.1 presents a code snippet to illustrate this situation. If the useCompressed condition is true, in module Rocket, the value of nBufValid, in module IBuf, is greater than 0, and the register buf.pc is connected to the output io.pc. As such, an additional pipeline stage is added, with the register buf.pc preceding ex_reg_pc. Otherwise, the register ex_reg_pc has at its input frontier io.imem.bits.pc, which is further connected to the register s2_pc. ----------------

- class IBuf val n = fetchWidth -1 if ( n == 0) then UInt(0) else Reg(fetchWidth)
io.pc := Mux(nBufValid > 0, buf.pc, io.imem.bits.pc) Our approach is developed at FIRRTL high form level. The high form compilation passes rely on the check and simplification transformations and do not modify the circuit as a propagation constant pass. Thus, the analysis is conservative as it considers both outcomes of the multiplexer condition, i.e., for compressed and uncompressed instructions. Therefore, it constructs a 6stage pipeline datapath model for Rocket, applying the max_case 1 . A com- plete construction of this model is presented in Section 6.2. This last possibility of case 1 presents an inaccurate result if the register has two sources connected and one of them is assigned in the same stage as the particular register. According to this, it will be placed incorrectly with the max_case 1 . This case refers to the backward edges presented in the forwarding mechanism when we can find connections between registers of the same and latter stages. In this case, the register source with the minimally assigned stage is not connected to all the sources of the register under assignment and the min_case 1 will be applied. We illustrate this case in Fig- The source registers dec_pc and ex_reg2 of ex_reg1 are already assigned, and the source register dec_pc precedes this source ex_reg2. So, the max_case 1 is applied, assigning the register ex_reg1 to the maximal stage plus 1. However, this is the result of an over-approximation. The register ex_reg1 should be located in the same stage as ex_reg2 since it is a part of the forwarding mechanism that must be completed with other sources in the latter stages, where the source with the minimal stage is not connected to all these other sources. Thus, the min_case 1 will be applied, and we assign the register ex_reg1 to the minimal stage plus 1.

Case 2 (lines 11-13) assigns a register r in the same pipeline stage as an already assigned register reg from the same context. Formally, the case 2 is applied when C2 is true, where

C2 = ctx_reg(r) = R ∧ ∃reg ∈ R ∧ to_stage(reg) = i.
Figure 6.4 illustrates in more detail an example of this case in the Rocket processor, namely the assignment of register ex_reg_inst, which is connected to an external module inst (i.e., that is not included in the considered datapath pipeline modules). ex_reg_inst is assigned according to this case 2 since it is collected in the same context as an assigned register ex_reg_pc, thus in the same stage as this register. The solution produced by our algorithm is the graph IR P with registers as nodes, for which pipeline stages have been assigned. Our algorithm is based on dependency relations between registers as well as an heuristic that considers the way the design is made. However, some registers may not be assigned to a pipeline stage due to the heuristic nature of our assignment algorithm that combines the various assignment cases defined before.

Therefore, the correctness of the algorithm is reduced to prove a subsumption relation relating the original processor design, say Q Pr and the solution P IR P of our algorithm. Precisely, Q Pr is the set of prec predicates, derived and evaluated with respect to a set of processor design executions and P IR P is the logical encoding (i.e., also as a set of prec predicates) of the transitions in the subgraph solution of our algorithm.

. Application to RISC-V Processor Designs

In the last section, we have presented the register assignment procedure described in the assign_regs function of Algorithm 3. This function, as mentioned before, maps registers in their pipeline stages. In this section, we illustrate the application of this procedure on different RISC-V Chisel-based processors with mono-module and multi-module datapath pipeline designs. The processor is made of 37 registers and we present, in Figure 6.6, some of these registers that we consider relevant. We specify that the if_pc register (i.e., the P C register) is located in the first pipeline stage. Our algorithm places the registers dec_pc, ex_pc and mem_pc into respectively consecutive stages as they are part of the same connected component of IR P with one register source (linear_case 1 , shown in Figure 6.8). Then, our algorithm assigns the register dec_inst as it is updated in the same context as dec_pc (using case 2 ). Indeed the frontier of the register context of dec_inst contains a reference to an external design element, the module IM (standing for the instruction memory).

Mono-module Pipeline

The next registers to be assigned are the forwarding registers ex_alu_op1, ex_alu_op2 and ex_rs2_data. They should be assigned with the min_case 1 since all these registers are connected to several source registers where there are no precedence relations between the source register of minimal stage dec_inst, and all other source registers (like the mem_alu_out, and wb_wbdata registers). However, their respective input frontiers contain registers that are not currently assigned (i.e., mem_alu_out and wb_wbdata), since they are part of the backward edges in blue color in Figure 6.6, coming from the data forwarding semantics. However, the context of register ex_pc contains these not assigned registers enabling the use of the case 2 of our algorithm. Finally, our algorithm places the remaining registers, i.e., mem_rs2_data with the linear_case 1 based on the register dependencies, and mem_alu_out with min_case 1 . The source registers of mem_alu_out, which are ex_alu_op1, ex_alu_op2, and ex_pc are already assigned in the same stage, and there are no precedence relations between all of them. Thus, mem_alu_out is assigned with min_case 1 . Therefore, the algorithm assigns the register wb_wbdata with the linear_case 1 based on the register dependencies. We summarize in Section 6.3, the experimental result of our algorithm application on the complete design of RISC-V Sodor 5-stage. Mono-module Pipeline Design -Kyogen RISC-V. We now illustrate how our pass analyzes a RISC-V processor, called KyogenRV [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF] in order to construct its abstract pipeline model. KyogenRV is an open-source 5-stage pipeline processor. More details of this processor are presented in Section 2.2. By our classification, it is a mono-module pipeline design. Our pass focuses on the top module of the pipeline, namely KyogenRVCpu, which has 108 registers, out of which we present the application of our algorithm only on a subset of registers, i.e., those linked to the PC register in Table 6.1 and Figure 6.7. Table 6.1 describes the register assignment phase on the KyogenRV processor. We assume that if_pc is the PC register and is placed in the first pipeline stage. Then our algorithm assigns the register id_pc_temp using the linear_case 1 , since it follows directly the source register if_pc. Our algorithm proceeds to assign the register if_npc with the case 2 since it is updated in the same context with the PC register. This enables the assignment of the register id_npc_temp with the linear_case 1 . Then, our algorithm assigns the register id_inst linked to an external module instruction memory using the case 2 as it is updated in the same context as the register id_pc_temp, fol-lowed with the assignment of the registers ex_inst and id_inst2_temp with linear_case 1 . Furthermore, the registers id_pc and id_npc are also assigned using case 2 , since they are connected to registers that are not already assigned. Then, the registers ex_pc, mem_pc, ex_npc, mem_npc, wb_pc are assigned into their respective pipeline stages with linear_case 1 , as they are part of the same connected component of the resulting intermediate graph.

The next registers to be assigned are ex_reg_raddr and ex_reg_waddr. Their respective input frontier includes the external module RegisterFile, so they are assigned with the case 2 relying on the same context with ex_pc. Then, the following registers mem_reg_waddr and wb_reg_waddr are assigned with the linear_case 1 .

The forwarding mechanism of the KyogenRV processor is implicitly implemented with wires that go through the external ALU module. So, the registers ex_rs,mem_rs, mem_alu_out are updated with the output of the module ALU, being assigned with case 2 . We present the abstract pipeline model of KyogenRV in Figure 6.7. It shows a subset of the identified registers and their dependencies (omitting the combinatorial circuitry). Our pass correctly identifies the 5 stages, with forwarding mechanisms from the WB and the MEM to the EX stage implemented with the blue edges (potentially merged). We details the statistics result in Section 6.3.

Reg to assign

Multi-module Pipeline Design -Rocket Processor

We detail now the abstract datapath pipeline construction of a multi-module pipeline design, that of the Rocket processor. This particular pipeline is specified in five Chisel modules Rocket, IBuf, FrontEnd, RocketTile, ShiftQueue when the first three modules contain the pipeline registers, and the last two are developed as interface modules. Table 6.2 details the execution of the register assignment algorithm (i.e., Algorithm 4) on the Rocket processor. Since this design is made of 240 registers, we choose to present only a subset of these registers. We start, as usual, with s1_pc, the P C register, assumed to be assigned in the first pipeline stage. Then, our algorithm proceeds to place registers s2_pc, buf.pc and buf.data into their respective stages using the linear_case 1 as these regis- ters are part of the same connected component of IR P . The most interesting case is that of register ex_reg_pc. Our algorithm proceeds to assign this register through the max_case 1 since its source registers s2_pc and buf.pc are already assigned to stages 2 and 3 respectively, and the source min s2_pc precedes the other source buf.pc. Then, the linear case 1 is applied in order to assign the registers mem_reg_pc and wb_reg_pc to their corresponding stages. The next registers to be assigned are ex_reg_cause and ex_reg_inst as their respective input frontier contains a reference to an external design element, the module Inst. So, these registers are assigned using case 2 as they are updated in the same context as ex_reg_pc. Then, our algorithm applies the linear_case 1 to assign pipeline stages to registers mem_reg_cause and mem_reg_inst, and further to registers wb_reg_cause and wb_reg_inst.

Furthermore, case 2 is applied to register mem_reg_wbdata, which is connected to an external design element, the module ALU and which is updated in the same context as mem_reg_pc. A similar case is the register wb_reg_wbdata, updated in the same context as wb_reg_pc, thus, case 2 is applied. Finally, our algorithm assigns the remaining registers ex_reg_rs0, ex_reg_rs1 to pipeline stages. More precisely, their respective input frontier contains a reference to an external design element, the module corresponding to the register file RF.

So these registers are assigned using the case 2 , as they are updated in the same context as the registers already assigned to the execute stage. Figure 6.8 shows the resulting pipeline datapath of Rocket, omitting those registers that are not on the path from the initial PC register.

. Experimental Results and Synopsis

We evaluated our analysis on several Chisel-based RISC-V processors. We consider our use case processors presented in Chapter 2, the mono-module designs such as RISC-V Mini [START_REF]Risc-v mini[END_REF], Sodor 5-stage [1], and KyogenRV [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF], and the multi-module structure as Sodor 3-stage [1], Fuxi [START_REF]Fuxi, a 32-bit pipelined risc-v processor written in chisel3[END_REF], and Rocket Chip [2].

Our evaluation is on a quad-core Intel Core i7 at 1.90GHZ and 16GB RAM memory. We report the results of our analysis in Table 6.3. Table 6.3 -Experimental results on RISC-V processor designs. The first column, LOC presents the code size of each pipeline P, while the second column, #M P indicates the number of pipeline modules, i.e., the cardinal number of P. Our analysis is applied over single and multi-module datapath pipelines. The first three lines in Table 6.3 report the processors made of a single module to implement its pipeline datapath, while the three last ones concern the multi-module pipelines. The next three columns report statistics related to the numbers of registers #Regs, of contexts #Cxts as well as the largest input frontier #F rt. This parameter is a measure of the maximal connectivity between a register and other design elements, either sequential or combinational. The next five columns detail the number of registers successfully assigned to pipeline stages. As such, columns linear_case, min_case and max_case report the number of placed registers by the respective case. Then, column Case 1 reports the aggregated results of these three cases including the PC register, and column Case 2 presents the number of registers placed by this particular case. Finally, the last two columns report the run time of our algorithm: the first corresponds to the intra-module phase (e.g., lines 2-5 of Algorithm 3), while the second corresponds to the register assignment phase (e.g., Algorithm 4).

The depth of each pipeline has been correctly computed, namely our approach constructs a pipeline datapath of the same depth as in the respective processor specification. Moreover, using the naming conventions with respect to register names and the pipeline stages (e.g., prefixes dec_ and ex_ or exe_ for decode and execute stage respectively, as shown in Listing 4.13 or Listing 4.16), we could also check that the registers are assigned in their expected pipeline stage.

We also encountered several issues. For example, our approach initially identified the KyogenRV design as a 7-stage pipeline instead of a 5-stage one. This over-approximation was due to the use of the Chisel RegNext construct. More specifically, the semantics of RegNext produces a one-cycle delayed version of the associated signal as described in Listing 4.8 in Section 4.3. At the FIRRTL level, it is translated into an additional register for each delay and thus an additional pipeline stage as there are two uses of RegNext in KyogenRV, as detailed in Listing 4.9 in Section 4.3. However, these registers can be identified based on their compiled FIRRTL names (i.e., a particular prefix is added), allowing us to discard them when building the IR P and then the assignment of registers.

Furthermore, our approach assigns all the registers of the pipeline modules only for two designs, Sodor 5-stage, and RISC-V Mini. For the KyogenRV processor, the unassigned registers are, in fact, not related to the datapath but to the control path as our algorithm also collected a vector register named rv32i_reg[0-31], implementing the register file. We present next an example of a control register called ex_ctrl.alu_op1 in Listing 6.3. This register is an element of the register ex_ctrl, which is a Bundle type IntCtrlSigs, lines 11-13 in Listing 6.3. Thus, all the fields of this class IntCtrlSigs, lines 2-6 in Listing 6.3, such as ex_ctrl.br_type, ex_ctrl.legal, ex_ctrl.alu_op1 and ex_ctrl.alu_op2 are registers defined in the control path and used in the datapath module. For Rocket and Sodor 3-stage designs, the control registers are generally defined as a compound type such as Bundle or Vector type. Thus, each field is considered an individual register and represented as such when the register assignment is performed. However, these registers are from the control path, updated in the external modules Exts, for instance, the modules CSR or BTB of Rocket. Indeed, Rocket is more complex, and modules have emerged that we have not yet considered. With these modules, we need to be able to link registers and, therefore, assign many registers. Sodor 3-stage and 5-stage are two variants of RISC-V Sodor, of which our algorithm assigns all the pipeline registers only for the 5-stage. This difference between the two variants of the same processor is due to their pipeline datapath structure. The Sodor 5-stage is a mono-module pipeline design. However, the Sodor 3-stage pipeline datapath is built on several pipeline modules.

We can also notice that the runtime of the assignment phase is significantly lower than the one of the intra-module phase. The latter increases with the number of modules, and thus, is the highest for the Fuxi processor. This runtime value for the intra-module phase summarizes all the iterations of the processor pipeline modules.

Next, we summarize in Figure 6.9 the execution steps of the register assignment, i.e., Algorithm 4, for all the processor designs. We illustrate the evolution of this assignment function when successfully assigning registers.

The coding color of the algorithm traces is also displayed in Table 6.3: green represents the linear_case 1 , gray and pink are min_case 1 and max_case 1 respectively, and orange represents case 2 . Furthermore, the multi-module aspect is also reported by specifying the transition between pipeline modules when assigning registers, using the symbol '↑'. We notice that the register assignment applies the linear_case 1 in the beginning as it is driven by the register dependencies. We also notice that the transition between modules exposes the way the implementation of the multi-module aspect is done in our analysis. For Fuxi, the flat module design results in frequent module changes, moving between pipeline stage modules and the MidStage module, as shown in Fig. 4.5. It is, however, not the case of Rocket and Sodor 3-stage. This is due to the hierarchical module design, shown for Rocket in Fig. 4.4, where the registers are restricted to three modules IBuf, Frontend and Rocket. More precisely, the registers of the stages PC-generator and IF, are implemented in the module Frontend while the registers of stages from ID to WB are in the module Rocket.

. Conclusion

The automatic generation of the abstract datapath pipeline models aims to identify the pipeline depth, and the pipeline stages from building associations of the register-to-pipeline stage. It is structured in two phases; the first phase concerns register analysis which outputs an intermediate representation of the datapath pipeline designs. The resulting graph is exploited in the second phase presented in this chapter.

In this phase, we focus on assigning registers to their pipeline stages.

We specify the first stage as being the stage where the PC register is placed.

Then we assign others according to two strategies; the first one is based on the dependencies between registers and the second on heuristics, based on when condition statements, which is used to determine additional relations between these registers. This heuristics is based on how the processor is coded. Furthermore, we have applied this analysis to various RISC-V Chiselbased processors with different pipeline depths ranging from 3 to 6 stages.

We have illustrated the resulting abstract datapath pipeline models for several processor designs. We have also summarized the result statistics and discussed the experimental results for each processor design. This thesis work aims to automatically build a framework from high-level designs to abstract models used then for different applications. Our purpose is to generate pipeline models for timing analysis of safety-critical systems. We present in the next Chapter 7 how to generate formal micro-architecture models from the generated abstract pipeline models with the goal of formally verifying timing-related properties such as the detection of timing anomalies. 111

-Automatic Construction of Formal Models From Abstract Models

The formal verification of timing properties over pipeline designs requires the construction of appropriate formal models. These models should consider the execution progress of the input program through the pipeline with cycle-accurate granularity thus, generating such infrastructure should be based on the abstract datapath model. As such, we aim to automatically generate formal models from the constructed abstract datapath pipeline models, seen in previous chapters, to which we then manually add the control path to capture the instruction flow through the pipeline stages.

We present in this chapter how to generate and then integrate formal pipeline models for the purpose of verifying timing properties of safety-critical systems such as those related to temporal predictability [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF][START_REF] Binder | The role of causality in a formal definition of timing anomalies[END_REF]. We start with detailing in Section 7.1, the formal model generation from the abstract pipeline datapath models. Then, we illustrate this generation on various RISC-V processor designs in Section 7.2. Finally, we present as a use case the integration of such formal pipeline models into an existing model checking-based procedure for the detection of timing anomalies in Section 7.3. Finally, we evaluate the impact of these semi-automatically generated formal models in this integration through a series of synthetic benchmarks.

. Formal Modeling of Processor Pipeline Designs

The formal model required should integrate both program and architecture features, where the program provides a sequence of instructions to be executed while the architecture adds timing to this sequence, e.g., counting clock cycles while instructions pass through a pipeline. A formal pipeline design should be based on both a datapath and a control path. In the following, we combine automatically-constructed datapath pipeline models detailed in Chapters 5, 6 with control path logic, to define the notion of pipelined execution. We also need to map the instructions, i.e., the input program, onto these abstract pipeline models so as to finish integrating both software and hardware aspects. The two abstract models (i.e., datapath and control logic) and the program representation are then translated into formal specifications using the TLA+ language [START_REF]The TLA+ Language and Tools for Hardware and Software Engineers[END_REF].

. TLA+ Specification from Datapath Pipeline Designs

We introduce next in, Listing 7.1, the skeleton and some notation elements of the TLA+ specification language to ease the understanding of the TLA+ code snapshots of the formal pipeline model that we introduce in this chapter.

Listing 7.1 -Template of a TLA+ formal model.

- ----------------------MODULE ModuleName------------------- ---------------------------------------------------------- A TLA+ model is organized as a collection of modules, as presented in Listing 7.1, where each module contains a module body. The body consists of a sequence of statements, which can be a declaration, definition, assumption or theorem. In order to build large hierarchical specifications, we can build a new module on top of other modules. One way to do this is with the EX-TENDS declaration at the beginning of the module, for example including M1, M2 in module ModuleName. The state variables are declared after the keyword VARIABLES.

We present next in Listing 7.2 the header of the RISC-V Mini TLA+ formal model. The formal model is described in module MODULE formal_model_mini.

The module includes other modules, such as the standard modules Sequences, Integers, TLC required to manipulate procedures, integers, and assertions. Furthermore, it includes the module Instructions defining a representation of the instruction set architecture (ISA). RISC-V Mini is a processor design with three pipeline stages. Thus, the state variables are built around these stages and currCycle variable to describe the cycle-accurate granularity.

Listing 7.2 -TLA+ snapshot code of RISC-V Mini -------------MODULE formal_model_mini ----------------------EXTENDS Sequences, Instructions, Integers, TLC CONSTANTS Program VARIABLES currCycle, stage_1, stage_2, stage_3 ------------------------------------------------------------... TLA+ allows us to specify the system through a single TLA+ formula containing, in particular, an initial-state predicate (Init) and a next-state relation (Next) built from actions, capturing the update of variables. More precisely, an action relates the values of variables in the current state x to their values in the next state x'. The specification could contain several other operators that can be parameterized and used later for the next-state relation. Furthermore, the TLA+ specification also contains the properties (i.e., temporal logic formulas) which are to be verified. We employ model-checking techniques, using the TLC tool [START_REF] Yu | Model checking tla + specifications[END_REF], to explore the TLA+ specification while verifying the required timing properties. The initial state and the next-state relation are defined through the next algorithms.

Algorithm 5 describes the formalization of a datapath pipeline model from the constructed datapath abstract pipeline model. Thus, we consider as input the resulting graph of the datapath pipeline generated with the approach described in Chapters 5, and 6 and an operator ElmtP rog to which the program is then assigned. The graph corresponds to the resulting registers-to-pipeline stages and their dependencies, IR P . The program assigned to the operator ElmtP rog represents a sequence of the instructions that are described according to the representation of the RISC-V ISA. We detail in Section 7.1.2 the corresponding representation. The algorithm output conforms to the formal specification of the datapath pipeline, formalized using the TLA+ language. Our TLA+ specification targets the execution of instructions through the pipeline stages with cycle-accurate granularity. Thus, we define first the state variables, in line 1, which includes the pipeline depth (i.e., pipeline stages, in variables Stages) and clock cycles defined in currCycle variable. Second, we distinguish two operators for our specification -initial and update. The initial operator InitP ipe, line 2 in Algorithm 5 initializes an empty pipeline described in formal_Init function detailed in Algorithm 6.

Thus, we consider the resulting graph of the datapath pipeline model Pregs, then we initialize each register in each pipeline stage with empty, lines 3-4 in Algorithm 6. We denote by R, line 4 in Algorithm 6 an operator to assign values to the registers and output TLA+ records Stage i _assign with fields being the registers assigned to the corresponding pipeline stage. The operator Stage_upd assigns the registers updated with empty to each pipeline stage. As mentioned, these fields are initialized with empty, where empty defines an empty content of a register. Then, we output the StageInit, which contains the TLA+ records of all the pipeline stages, lines 4-5 in Algorithm 6.

The update state is produced with the formal_Next function, line 5 in Algorithm 5. This function is detailed in Algorithm 7. We model the pipeline update where each stage update is modeled by an action on its registers and their dependencies. We consider the corresponding dependencies graph IR P . We check the registers assigned with the max_case 1 as they are speci- fied in MaxCaseRegs function, line 3 in Algorithm 5. Then, we only keep in the IR P graph its register dependency, which corresponds to the maximal stage, line 3-4 in Algorithm 7. Since the IR P graph includes all the dependencies between registers, for the register assigned with the max_case 1 which has two register sources, we only keep the dependency corresponding to the register with the maximal stage. Indeed, this choice is not fortuitous, it is consistent with the WCET analysis, where we consider the longest path. Afterward, we update each stage by updating its pipeline registers, line 5 in Algorithm 7. We update the register PC of the first stage with the first instruction of the input program, lines 6-8 in Algorithm 7. Furthermore, we consider the registers for other pipeline stages and update each register with its dependencies, lines 9-26. We distinguish between three cases. The first case describes the register without dependencies, it is updated with empty content, lines 11-12. We denote by Reg_updt an operator to assign a value to the register. The second case targets the registers placed with the linear case, lines 13-15. The register is updated with the value of its source register using the function MapStage. This function takes two arguments: the pipeline stage of the source register and the source register, then it outputs the value of type string for updating the register, line 14. Finally, the last case updates registers with multiple dependencies, lines 16-26. Thus, we present next the dependencies related to the control conditions for each register, line 17. We address first the conditions associated to the forwarding mechanism and defined in bypass_cond operator, lines 19-21, then, we specify the other conditions specified in select_cond operator, lines 23-24, which are all to be evaluated to true or false according to the execution pattern of the instructions.

We note that all the registers dependencies used as a selection relation in the combinatorial logic do not exist in the update state of the registers, line 4 in Algorithm 5 and line 19 in Algorithm 7. Since these registers are used in the combinatorial components (e.g., multiplexers) in selection conditions, our algorithm removes all these dependencies from the graph IRp to represent in the formal model. Since our approach that generates the datapath pipeline model outputs more register dependencies (over-approximation), the analysis does not include the combinatorial logic that distinguishes between the selection and data dependence relations. Afterwards, we output the TLA+ record in StageUpdate variable, which contains a record of each pipeline stage R defined in Stage i _assign variable, lines 26-27 in Algorithm 7.

Our TLA+ specification Spec is defined with an initial state Init and a state transformer Next as follows:

Spec == Init /\ [][Next]_<< State_var >>
The initial state is a conjunction between the resulting empty pipeline stages defined in InitPipe and the remaining state variable currCycle:

Init == /\ InitPipe .... /\ currCycle = 0
The transition state is also defined as a conjunction between the update of pipeline stages and currCycle variable for an ideal pipeline as follows:

Next == ... /\ UpdatePipe ... /\ currCycle' = currCycle + 1

The TLA+ specification integrates both the datapath and control path of the pipeline. Thus, each action, Init and Next integrates the generated pipeline stages and the control path to define the execution and entail changes in the datapath process.

. Control and ISA Modeling TLA+ Specification

In our workflow described in Figure 4.1, the TLA+ formal models are based on the abstract pipeline models and the program executed on this pipeline. We add the control logic to the automatically constructed model of the datapath pipeline. The control path manages the control of data movement between components in the pipeline. Since we aim to build pipeline models for timing analysis, we should integrate how instructions advance through this pipeline model so as to prove the timing properties. Currently, the integration of the control path is mainly manual, as is the abstract Instruction Set Architecture (ISA) semantics for the same design. The Program component, defined in figure 4.1 and introduced at the beginning of Algorithm 5 as input, is responsible for defining ISA-level execution patterns on the constructed pipeline model, describing the necessary infrastructure to reason about timing properties of the design.

The control logic addresses all the signals that ensure that data flow into pipeline stages and that instructions are properly executed. It includes the selection signals of combinatorial and sequential circuitry: multiplexer, functional units, registers, etc. These signals are related to the instruction patterns and are designed to determine pipeline status such as stalling, branching logic etc. These execution patterns are specified as a set of control conditions defined in pipeline update UpdatePipe. While their placement is automatically generated, their actual semantics is added by hand. Pipeline status determines the progress status of the execution. Thus, in order to correctly add the control logic, we need to specify the ISA instructions of the processor, then analyze the implementation of each instruction to determine the placement of control points that affect the register transfer, and finally examine the input program to define pipeline status (stall, kill, etc).

We also need to introduce the abstract RISC-V ISA modeling which is specified also by hand. The abstract ISA consists of a set of instructions grouped in classes, sharing the same execution patterns, expressed in the form of a set of conditions conds as follows: The example above describes three types of instruction classes. Adding to selection conditions specified in conds, the description of the instructions also exposes the source and destination registers, rs1/2 and rd respectively, initialized with some default values. We specify in TLA+ these instruction operands to express the dependencies between instructions and then identify the forwarding mechanism. Then, we define the bypass conditions bypass_cond by comparing the instruction operands defined in the registers rs1, rs2, and rd. We detail the semantics and the body of these conditions in the application case studies in Section 7.2. Now for the pipeline status, we model the stalling logic. This stalling logic is also defined by hand and based on how the pipeline interacts with the memory system. For example, we could encode such a logic that stalls the pipeline for five cycles whenever there is memory access caused by load/store instructions. The predicates stall and stall_cond state exactly this behavior. stall == stage_MemStage.MemStage_pc.inst.type = "lw" \/ stage_MemStage.MemStage_pc.inst.type = "sw" stall_cond == stall /\ stall_delay < 5

The pipeline stages with the stalling logic are modeled in StallPipe operator and described in formal_Stall function in Algorithm 8. We specify the pipeline stall from the first stage until the stage for the memory access defined in MemStage variable, line 4. We stall the pipeline for the memory latency cycles for all the pipeline stages before the memory stage, lines 4-7, and we keep the other stage advancing through the pipeline, we update all the registers in this pipeline stage with empty, in Stage i _assign line 8. Then, we output the pipeline stages on the stalling state, lines 9,10 in Algorithm 8. The state transformer of Spec is refined with the Stall as follows:

Spec == Init /\ [][TransPipe \/ Stall]_<< state_vars >>
As such, we distinguish between two types of pipeline progress: pipeline progress when there is stalling, via Stall and pipeline progress without stalling, using Next. This modeling accounts for the hardware part of the specification.

Then, in this modeling we map the input program, given as a sequence of instructions (specified by the abstract ISA) and having the conditions to guide their execution through the pipeline. This is the software aspect of the formal model.

. Application to RISC-V Processors Case Studies

RISC-V Sodor 5-stage Pipeline. We detail next our formal model for the pipeline of the Sodor 5-stage processor; this model combines an automatically generated datapath with manual extensions for the control and ISA-level semantics. We refer to each aspect in the following description. Our TLA+ specification Spec is defined with an initial state InitPipe and a transition states defined with TransPipe and StallPipe as follows:

Spec == InitPipe /\ [][TransPipe \/ StallPipe]_state_vars
The state variables include the pipeline depth of RISC-V Sodor 5-stage and the cycle level granularity, which corresponds to:

state_vars = << stage_1, stage_2, stage_3, stage_4, stage_5, currCycle >>
The initial state is an empty pipeline. Thus InitPipe contains the initialization of the pipeline stages. We present next the registers of stage 3, which correspond to the registers described in Figure 6 The update of register ex_alu_op1 is defined with respect to the set of dependency relations between registers, where each possible update is guarded by a condition bypass_cond or select_cond as specified in the Algorithm 7.

Each condition is associated with the corresponding source register defined in Updt with the function MapStage in the Algorithm 7. For example, for the update of register ex_alu_op1 with the source register wb_wbdata, it corresponds to the value stage_5.wb_wbdata. The condition bypass_cond is defined for each register as bypass_x_y, while select_cond as cond_z. These conditions correspond to the blue and, respectively, black edges of the datapath from Figure 6.8. More precisely, the ISA model defines, for each instruction class, an execution pattern on the pipeline in the form of a set of conditions cond_z. Now, the semantics of cond_z is as follows: given an instruction i in a pipeline stage, if the progression of i is conditioned by cond_1, then cond_1 evaluates to true only if it is among the stated conditions of the instruction type of i. The semantics of bypass_x_y is also given by hand and states the true data dependencies, using the registers rs1, rs2 and rd of instructions found in the pipeline stages x and y as follows:

bypass_3_3 == stage_2.dec_pc.inst.RS1 = stage_3.exe_pc.inst.RD bypass_3_5 == stage_2.dec_pc.inst.RS1 = stage_5.wb_pc.inst.RD bypass_3_4 == stage_2.dec_pc.inst.RS1 = stage_4.mem_pc.inst.RD

For the stalling logic, it is integrated with the operator StallPipe with stage_4 as the assumed memory access stage in the case of the Sodor 5-stage pipeline. The memory stage is added manually. We stall the pipeline stages from stage_1 to stage_4 with UNCHANGED, as defined in stageStall variable in the Algorithm 8. The write-back happens in stage_5 where instructions can leave the pipeline and the register wb_wbdata is updated with empty as explained in the Algorithm 8, line 8.

StallPipe == /\ stall_cond /\ stage_5' = [ wb_wbdata |-> empty ] /\ stall_delay' = stall_delay + 1 /\ currCycle' = currCycle + 1 /\ UNCHANGED << stage_1, stage_2, stage_3, stage_4>>
Rocket Pipeline. We illustrate now the formal model for the pipeline of the Rocket processor. The pipeline depth of Rocket is 6 stages. Thus, the state variables are defined as follows:

state_vars = << stage_1, stage_2 , stage_3, stage_4, stage_5, stage_6, currCycle >>
We model the pipeline update where each stage updates the registers according to their dependencies. As detailed in Algorithm 5, line 3, we consider the corresponding graph of the register dependencies IRp with only the longest path in the max_case 1 dependencies. Rocket processor presents the max_case 1 to assign the register ex_reg_pc as detailed in Figure 6. We next illustrate the ISA model for two instruction classes to map the input program into the pipeline models to finish integrating both software and hardware aspects of formal models. We model the update of stage 6 with only one register. The following TLA+ description corresponds to the datapath pipeline model in Figure 6.8. The input program is a sequence of instructions. Thus, we follow the progression of each instruction on the pipeline. For example, when an instruction i is in a pipeline stage, if it is a jump instruction, then cond_1 is evaluated to true since cond_1 is among the stated conditions of the jump instruction type. Thus, we semi-automatically generate the formal models from the processor designs. Indeed, we automatically generate the datapath pipeline models and add the control logic by hand to guide the execution. Furthermore, we have also generated pipeline models for various RISC-V processor designs such as Sodor 3-stage, RISC-V Mini [START_REF]Risc-v mini[END_REF], Kyogen [START_REF] Saitoh | Kyogenrv: simple 5-staged pipeline RISC-V[END_REF], Rocket [2] and Fuxi [START_REF]Fuxi, a 32-bit pipelined risc-v processor written in chisel3[END_REF]. Fuxi 297 32 90%

Table 7.1 presents statistics related to the manual and automatic lines contained in the TLA+ specification for each processor design. The automatic LOCs include the generated datapath model, while the manual LOCs include the control (stalling) and the map of the input program into the TLA+ specification. For instance, the TLA+ specification of the RISC-V Sodor 5-stage pipeline is around 170 lines out of which, 145 lines are automatically generated and only 25 lines are added by hand. Furthermore, the number of automatic lines is related to the size of the intermediate graph (i.e., pipeline registers). It increases for the designs with a large number of pipeline registers assigned in their pipeline stages, as for KyogenRV and Fuxi processor designs.

Next, we present the impact of control logic (i.e., the pipeline stalling) which was added manually on the TLA+ specification. We report in Table 7.2 the results for various processor designs, where we evaluate the impact of checking for stalling conditions, on the TLC running time with a property as a currCycle is lower than 1000. We design by processor_complete the formal specification of both datapath and control logics, while the processor_datpath reports the results for only the datapath formal model. The formal pipeline models are built to address the execution of basic blocks, basically, not very long sequences of instructions. Thus, the input program size on which we experiment is relatively small, up to 200 instructions. We can observe that adding the stalling logic in the TLA+ specification increases the runtime for all the processor designs. The evaluation includes the stalling conditions and the pipeline progress in the case of the stalling.

. Integration of Formal Pipeline Models in a Timing Anomaly Detection Procedure

We detail next the integration of the generated pipeline models into an existing model checking procedure for the detection of timing anomalies. We start with presenting the corresponding definition of timing anomalies and its TLA+ formal encoding. Then, we report the evaluation synthesizes of the integration through various benchmarks, on a number of RISC-V processor designs.

. Model Checking for Timing Anomalies

Static WCET analysis can be complicated by the presence of an undesired timing phenomenon called timing anomalies [START_REF] Lundqvist | Timing anomalies in dynamically scheduled microprocessors[END_REF]. Indeed, they are a threat to the computation of safe bounds, thus it is necessary to explore all the paths 125 in order to compute bounds. A timing anomaly is a counter-intuitive timing behavior in the sense that the local worst-case timing behavior does not result in the global worst-case performance. Figure 7.1 illustrates the timing anomalies definition on two executions, in this case, it is a counter-intuitive timing anomaly.

Timing anomalies can be produced from shared resources between architecture components or an unpredictable timing behavior coming from the interaction with the memory system. Reasoning about timing anomalies means reasoning on pairs of different execution traces corresponding to the same input program. Thus formal models of both the architecture and the input program are required. In our work, we consider the variabilities in execution latency resulting from the interaction between the pipeline and the memory system. Moreover, we integrate our semi-automatically generated pipeline model into an existing procedure for the detection of timing anomalies [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF], which encodes a definition of timing anomalies based on the concept of locality, proposed in [START_REF] Reineke | A definition and classification of timing anomalies[END_REF]. More specifically, this work defines a timing anomaly regarding local and global variations.

We illustrate next this integration of the semi-automatically generated state pipeline model. We define first a state_vars extension to capture local and global timing variations as part of a new state variable, asi: local variation defined by delta, global variation identified with ET specified for two traces. pcid and pathid rely to the program representation. We define their semantics later.

asi = [ delta |-> [n \in 1..2 |-> 0], ET |-> [n \in 1..2 |-> 0], pcid |-> Program.did, pathid |-> 1]
A timing anomaly is characterized by a pair of execution paths when we compare the local worst-case variations array (i.e., delta) with the global worstcases array (i.e., ET). The formal pipeline model should be evaluated on two traces, where each trace is a sequence of instructions, according to the insts definition provided in Section 7.1.2. Each instruction is represented by several parameters, the program counter pc, the instruction type in which we specify the operands inst, and the latency lat (to model the variability which is coming from the interaction with the memory system). Finally, the procedure for the detection of timing anomalies evaluates the pair of traces, given in fst and snd fields and specified in asi.pathid field to be initialized with the first trace, and with a locality defined whenever the instruction with pc given in field did is in a particular pipeline stage (e.g., stage_3). We define in the asi.pcid field the instruction identified in did program field.

Program <-[ fst |-> << [ pc |-> 1, lat |-> {1, 10}, inst |-> [type |-> "alu" ... ] ], [ pc |-> 2, ... ], ... >>, snd |-> << [ pc |-> 1, lat |-> {1, 10}, inst |-> [type |-> "alu" ... ] ], [ pc |-> 2, ... ], ... >>, did |-> 2 ]
The update state is extended to integrate the locality in instruction executions. The previously defined operator TransPipe of Sodor 5-stage is extended to fully explore the instruction latencies of an instruction in stage_2, before entering the locality-related stage, i.e., stage_3. Moreover, TransPipe is also extended with the corresponding update of the asi state variable, based on the system state (i.e., the self-explanatory conditions condFlushWB and not moreIns) as follows:

TransPipe == \exists lat \in stage_2.dec_pc.lat :

... Once the first trace fst is explored, the procedure for the detection of timing anomalies reloads the second trace snd, extending the specification with the following straightforward operator Reload:

Reload == condReload /\ ... /\ asi' = [ asi EXCEPT!.pathid = 2 ]
Where the corresponding conditions for Sodor 5-stage are defined as follows: condFlushPip == stage_5.wb_pc.pc = 0 /\ stage_4.mem_pc.pc = 0 /\ stage_3.exe_pc.pc = 0 /\ stage_2.dec_pc.pc = 0 /\ stage_1.if_pc.pc = 0 condFlushWB == stage_4.mem_pc.pc = 0 /\ stage_3.exe_pc.pc = 0 /\ stage_2.dec_pc.pc = 0 /\ stage_1.if_pc.pc = 0 condReload == /\ asi.pathid = 1 /\ ~moreIns /\ condFlushPip condFlushWB is used to update the global variation ET when the last instruction is in the last pipeline stage (write-back), and there is no more instruction in the input program to progress. condFlushPip is defined in order to reload the second program trace snd, where all the instructions of the first trace fst are already left the pipeline. As a consequence, The TLA+ formal specification Spec is extended and becomes:

Spec == InitPipe /\ [][TransPipe \/ StallPipe \/ Reload]_<< state_vars >>

. Experimental Results

The integration of the generated formal pipeline models into an existing procedure for the detection of timing anomalies allows us to evaluate the effectiveness of our work. As such, we evaluate its impact on all of the previously considered RISC-V processor designs, with their different characteristics, including the number of datapath pipeline registers, the pipeline depth, and the execution patterns specified with the tuple (instructions, control conditions). Furthermore, we evaluate also the path/condition coverage of the models through various instruction classes. We also measure the model checkingbased exploration of the state space in both its width and depth. The depth of the state space is expressed through a variation in the size of the input traces (i.e., instruction sequences), while the width of the state space is impacted by the latency variations of various instructions in the input traces. We detail next the evaluation of the processor designs.

We experiment with our integration procedure on two processor designs, RISC-V Sodor 5-stage and Rocket. We select these two due to their complexity and variety in terms of execution patterns and the pipeline structure, which is mono-module for RISC-V Sodor and multi-module for Rocket design.

The TLA+ specification of the RISC-V Sodor 5-stage pipeline, integrated into the procedure for the detection of timing anomalies, is about 320 lines, while it is composed of 250 lines for the Rocket processor. We then employ the TLC model checker to explore all the latency variations on the traces and detect timing anomalies. The input traces are synthetic benchmarks featuring variable latencies on various instructions and which are explainable by external static cache analyses [START_REF] Lv | A survey on static cache analysis for real-time systems[END_REF] or measurement strategies [START_REF] Kosmidis | Measurement-based timing analysis of the AURIX caches[END_REF].

We conduct experiments on three variants of each considered processor. First, a simple version where each pipeline stage is represented by a single register. This model is also used in [START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF] and named simple in our experimental evaluation. Second, the pipeline from Figure 6.6 and Figure 6.8, which are a subset of the (semi-)automatically generated pipeline model of Sodor RISC-V 5-stage and Rocket respectively, named processor_subset in the experiments. Finally, the complete pipeline model which is presented in Section 7.2 and named processor_complete in the following.

The experimentation is conducted on a quad-core Intel Core i7 at a frequency of 1.90GHZ and 16GB RAM memory and with the TLA+ Toolbox using the TLC model checker version 2.16. We summarize in Tables 7.3-7.8 the experimental results for multiple test scenarios. The overall goal is to measure the impact of the generated pipeline processor_complete (over processor_subset and simple implementations) on synthetic traces with and without timing anomalies. The general format of these tables is seven columns. We specify in the first column the pipeline models, in the second the corresponding size of pipeline registers, and in the third and fourth columns, some trace-related statistics namely, the trace size and number of different execution traces due to latency variations. The last three columns are model checking statistics, on the running time (the fifth column) and on the search space (the sixth column on the size of the longest behavior and finally the seventh column on the number of all states). First, we conduct experiments on proving the absence of timing anomalies, shown in Tables 7.3, and 7.4, with respect to a given scenario, detailed next. We consider a synthetic trace of 200 instructions in which we specify a pair of latencies for the instruction of interest (i.e., corresponding to hit/miss cache activity) as well as other arbitrary latencies for the rest of the instructions. Then, we employ bounded model checking with a bound of 1000 cycles, roughly established in a worst-case scenario wrt. the provided latencies and instructions. Then, the TLC model checker fully explores the state space, proving the absence of timing anomalies up to the provided bound with respect to the considered scenario. Next, we present, in Tables 7.5-7.8, results when timing anomalies are detected. We have experimented with several synthetic benchmarks with variable execution trace size as described in Tables 7.5, and 7.6, and with variable instruction latencies, reported in Tables 7.7, and 7.8 for Sodor 5-stage and Rocket respectively. The trace size is gradually increased, from 40 to 200 instructions, corresponding to reasonably-sized basic blocks, producing differences in the running times between simple and processor_complete models for longer traces (i.e., measuring the impact on the depth of the state space, in Tables 7.5, 7.6). Then, we fix the trace size to 200 instructions and increase the number of variabilities due to instruction latencies, up to 4M different scenarios, which are explored by the TLC model checker. This experimentation also reports runtime differences between simple and processor_complete, which are proportional with respect to the number of exposed scenarios, measuring the impact on the width of the state space.

We can observe for all Tables 7.5-7.8 the variable trace sizes and, more precisely, instruction latencies significantly impact the running time for the three pipeline variants. Indeed, the processors differ in the number of pipeline registers that construct the pipeline stages as the state variables. However, the statistics on the diameter and number of states found by the TLC model checker are similar for the three pipeline variants. The reason is that we execute the same sequence of instructions for the same number of pipeline stages, and the state variables are pipeline stages that group registers and not individual registers (which could lead to different state updates). Furthermore, the stalling logic is also the same for the three variants of the same processors, focusing on blocking the pipeline up to the memory stage. Thus, the difference between the pipeline variants relies on the pipeline registers that are included in the pipeline stages as the state variables. Moreover, the state variables' size is not changed. Therefore, the variability directly impacts the runtime and keeps the same diameter and states found for the three variants.

We have experimented with various complete versions of the processor designs with different pipeline depths from 3 to 6 pipeline stages with different sizes of the intermediate graph representation from previous chapters. Table 7.9 presents the experimental result with 200 instructions in the input program and a variability of 4M scenarios explored by the TLC model checker. These benchmarks report runtime differences between all these pipeline designs, which are related to different parameters: the pipeline depth, 3 stages for Sodor 3-stage and RISC-V Mini, 5 stages for Kyogen, and Fuxi, and finally 6 for Rocket. Furthermore, it depends also on the number of registers containing the graph and their updates according to control conditions and bypassing dependencies. For instance, the TLA+ specification of the processors Kyogen and Fuxi takes longer to run than the other processors with 5 stages, this is due to their pipeline registers assigned in the graph as reported in Table 6.3. The depth of state space (i.e., the diameter) increases with the pipeline depth. For example, it can reach 828 for processors with 3 pipeline stages: RISC-V Sodor 3-stage and RISC-V Mini, 832 for Kyogen, Sodor 5-stage, and Fuxi pro- cessor designs with 5 stages, and 834 for Rocket processor with 6 stages as a pipeline depth. Finally, the state founds number depends on state space depth (traces) and width (variabilities) and increases with the pipeline stages. Indeed, it can reach 2K of difference between 3 and 5 pipeline stages.

Integrating our formal pipeline models into a procedure for the detection of timing anomalies has demonstrated the effectiveness of the automatic generation of pipeline models from the code of processor designs. We have man- aged to demonstrate this integration by proving the absence/presence of timing anomalies on all our use case design processors. The absence is obviously proved with respect to the considered traces. Furthermore, we can produce reliable coverage for each processor's formal model with various benchmarks featuring variable latencies and multiple traces. The code coverage relies on the coverage of all the execution patterns provided by the Instruction Set Architecture (ISA) abstraction as control conditions specified by hand in the corresponding ISA module. The code coverage is achieved at runtime when all the conditions (i.e., bypass and control conditions) are tested and evaluated through relevant benchmarks. For instance, with a trace size of 200 instructions and 4M execution paths due to latency variation, we can reach the coverage of all the instruction classes and pipeline status. As observed, formal verification of properties on the provided models shows the impact of the automatic generation on the runtime and the state space size. The TLC model checker needs more time and faces the state space explosion proportionally with the complexity of the processor designs in terms of its number of pipeline stages, the pipeline structure, and the number of registers. Furthermore, the scalability of the automatic models remains reasonable compared to the simple ones.

. Conclusion

The timing analysis of safety-critical systems relies on hardware models (e.g., caches, pipelines, etc.); thus, generating pipeline models, wherever possible, is necessary. We have presented in this chapter the integration of such pipeline models into an existing model checking-based procedure for the detection of timing anomalies. Our proposed approach is based on a semiautomatic generation of pipeline datapath models from processor design code, which is then used to produce formal pipeline models. Then, we manually add to the datapath pipeline model the control logic (stalling), forming complete pipeline models that could capture the execution of instructions through a pipeline.

We have presented first the algorithms of the automatic generation of datapath formal models in TLA+. Then, we have illustrated the approach to various RISC-V processor designs. Thereafter, we experimented with their TLA+ formal specifications, integrated into a procedure for the detection of timing anomalies. We have reported preliminary experimental results in which we detailed the impact of the semi-automatic generation of pipeline models on the running time and state space explosion through several synthetic benchmarks. 135

-Conclusion and Perspectives

In this thesis work, we have presented our general workflow that addresses the formal verification of timing properties with the goal of automatic generation of formal pipeline models from high-level hardware designs. We have proposed an approach to automatically generate the pipeline datapath models for WCET analysis. It addresses the hardware design developed with Chisel language and integrated into the Chisel/FIRRTL hardware compilation framework. The approach considers as a starting point the datapath pipeline modules and relies on how the design is coded. The datapath pipeline modules can be an individual module defined as a mono-module pipeline design or is developed over several software-level modules as the multi-module pipeline, connected through interfaces and using various internal structures to define the pipeline circuitry. The analysis is structured into two main phases; the register analysis and then the construction of the abstract datapath pipeline model phases. Register analysis constructs an intermediate representation graph of the datapath pipeline as a dependency registers relation. The analysis is performed through two kinds of relations, the intra-module analysis and the inter-module analysis. The intra-module relations are performed at each module level for the register context. In contrast, the inter-module relations construct the input/output interfaces between pipeline modules in order to build the register connections. The second phase builds the abstract datapath pipeline model through a register-assignment procedure.

We have shown how a high-level hardware compilation toolchain can ease the adaptation of automatically generated formal abstract models to such safety properties. We have reported on a custom pass to generate an abstract pipeline model to be used therefore for the detection of timing anomalies. We have evaluated our approach on several in-order RISC-V processors, from the less to more complex range of processors, mono-module and multi-module of datapath pipeline. We have demonstrated the efficiency of our approach with various experiments that summarize the results and construct the synthesis.

We have also presented the automatic generation of formal models for the verification of timing predictability-related properties. These formal models are based on the generated datapath pipeline models in which we add control logic manually. We have translated the models into formal specifications using TLA+ language. This specification is further integrated into an existing procedure for the detection of timing anomalies. We experimented with TLA+ formal specification using the TLC model checking technique to explore the TLA+ specification while verifying the required timing properties. We have reported the experimental results in which we detailed the impact of the semi-automatic generation of pipeline models on the running time and state explosion through several synthetic benchmarks.

As future work, we aim to validate the results of our algorithm that constructs the datapath pipeline models against processors so as to replace the current manual validation of these models with an automated procedure. Our model is a subgraph of the original pipeline processor. The objective is to validate the models against the original processor through the processor execution of assumed programs. Thus, we combine our static construction with a dynamic analysis through program execution. Several techniques can be used in order to establish this dynamic aspect. We aim to test the design and simulate the execution traces. Therefore, the reliability of our model can be determined by proving that such a subsumption relation between our model subgraph and the results of the processor design execution exists. We compare the register relations of the original processor execution traces with the abstract model relations.

We also intend to evaluate our approach on more complex processors as out-of-order RISC-V designs. Out-of-order processors add more complex pipeline constructions and mechanisms as structural hazards and speculative execution. As such, we need to include and treat all the Chisel language constructions as queues to correctly approximate the hardware designs' timing behavior. Furthermore, analyzing out-of-order processors allows us to add several design components as functional units on pipeline models. This feature enables extending the detection of timing anomalies analysis.

-Annexe: Résumé Substanciel

Les systèmes embarqués sont conçus avec des fonctionnalités spécifiques et intégrés dans des systèmes plus complexes. Les systèmes embarqués disposent d'une infrastructure matérielle (basée sur un processeur) et sont capables d'exécuter des applications qui répondent à ces fonctionnalités spécifiques. Ces systèmes sont utilisés dans divers contextes allant des appareils portables aux systèmes critiques. La validité de ces systèmes critiques dépend non seulement de leur correction fonctionnelle, mais aussi du temps dans lequel ils sont exécutés. La conception de ces systèmes repose sur des réglementations et des normes pour aider à identifier et à traiter les événements dangereux potentiels. Par exemple, des événements tels que le non-respect des délais seraient jugés inacceptables pour ces systèmes.

Les analyses statiques de pire temps d'exécution sont parmi les approches utilisées pour garantir les délais requis pour les systèmes critiques. Afin d'estimer des bornes précises sur ces temps d'exécution, ces analyses nécessitent de modéliser très finement le comportement temporel de la microarchitecture du ou des processeurs utilisés dans la plateforme matérielle. Ainsi, ces limites sont exprimées en cycles de processeur. Ces modèles de micro-architecture sont aujourd'hui développés de manière manuelle, à partir d'éléments de documentation des processeurs qui peuvent être face à des erreurs. Cependant, avec l'émergence du design des processeurs open-source, dont les descriptions au niveau RTL sont disponibles, et les langages de description de matériel de haut niveau (HCLs), la génération automatique de ces modèles de micro-architecture et, plus spécifiquement, des modèles de pipeline permet d'envisager une automatisation de cette étape.

Nous proposons un workflow pour la construction de modèles de chemins de données de pipeline à partir de conceptions de processeurs décrites dans des langages de construction de matériel (HCLs). Nous intéressons aux conceptions exprimées avec le langage Chisel qui est supporté par la chaîne de compilation matériel Chisel/FIRRTL. La conception exprimée en Chisel est compilée par la suite en une représentation intermédiaire FIRRTL par le biais des transformations dont cette infrastructure dispose. Ces chaines de compilation facilitent l'intégration des analyses des conceptions matérielles. Notre workflow est basé sur cette chaîne de compilation Chisel/FIRRTL. Nous déployons des analyses qui visent à construire automatiquement au niveau de la représentation intermédiaire FIRRTL des modèles de pipeline du chemin de données.

L'approche prend donc comme un point d'entrée les modules de pipeline du chemins de données et s'appuie sur la manière dont la conception est codée. Nous visons par la suite l'utilisation de ces modèles pour des pro-priétés temporelles. Nous nous intéressons donc à l'aspect temporel au niveau du pipeline pour construire ces modèles. De ce fait, on construit le modèle de chemin de données de pipeline autour des registres. Nous présentons les résultats préliminaires de l'application sur plusieurs processeurs RISC-V opensource. Ces conceptions des processeurs sont caractérisées par leur diversité au niveau de nombre d'étages de pipeline et leur complexité de la structure du chemin de données du pipeline.

Nos travaux de thèse vise à appliquer ces modèles générés pour prouver des propriétés temporelles, notamment des propriétés liées à la prédictibilité temporelle. Pour prouver ces propriétés, diverses méthodes peuvent être utilisées. Nous adoptons la vérification formelle qui est une méthode exhaustive qui garantit que des résultats corrects sont produits dans toutes les conditions d'exécution possibles, et qui nécessite la construction de modèles formels. Les modèles générés sont suffisamment complets et précis pour être utilisé comme entrée pour la partie formelle. Nous les traduisons donc en modèles formels. Nous illustrons par la suite cette génération sur différents modèles de processeurs RISC-V.

Par ailleurs, nous les intégrons dans une procédure existante de détection des anomalies temporelle comme cas d'utilisation. Cette procédure est basée sur la vérification formelle. Nous employant le langage de modélisation et de vérification TLA+ et le model checking, et expérimentons notre analyse avec plusieurs processeurs RISC-V open-source. Nous évaluons cette intégration pour plusieurs processeurs comme cas d'étude. Nous examinons également l'impact de la génération automatique de modèles par le biais d'une série de critères synthétiques.

Résumé:

Les analyses statiques de pire temps d'exécution sont utilisées pour garantir les délais requis pour les systèmes critiques. Afin d'estimer des bornes précises sur ces temps d'exécution, ces analyses temporelles nécessitent des considérations sur la (micro)architecture. Habituellement, ces modèles de micro-architecture sont construits à la main à partir des manuels des processeurs. Cependant, les initiatives du matériel libre et les langages de description de matériel de haut niveau (HCLs), permettent de réaborder la problématique de la génération automatique de ces modèles de micro-architecture, et plus spécifiquement des modèles de pipeline. Nous proposons un workflow qui vise à construire automatiquement des modèles de chemin de données de pipeline à partir de conceptions de processeurs décrites dans des lan-gages de contruction de matériel (HCLs). Notre workflow est basé sur la chaine de compilation matériel Chisel/FIRRTL. Nous construisons au niveau de la représentation intermédiaire les modèles de pipeline du chemin de données. Notre travail vise à appliquer ces modèles pour prouver des propriétés liées à la prédictibilité temporelle. Notre méthode repose sur la vérification formelle. Les modèles générés sont ensuite traduits en modèles formels et intégrés dans une procédure existante basée sur la vérification de modèles pour détecter les anomalies de temps. Nous utilisons le langage de modélisation et de vérification TLA+ et expérimentons notre analyse avec plusieurs processeurs RISC-V open-source. Enfin, nous faisons progresser les études en évaluant l'impact de la génération automatique à l'aide d'une série de critères synthétiques.

Title: Formal Semantics of Hardware Compilation Framework Keywords: Modeling of processor design, Hardware Construction Languages (HCLs), Pipeline datapath, Timing anomalies, Model checking Abstract: Static worst-case timing analyses are used to ensure the timing deadlines required for safety-critical systems. In order to derive accurate bounds, these timing analyses require precise (micro-)architecture considerations. Usually, such micro-architecture models are constructed by hand from processor manuals. However, with the open-source hardware initiatives and high-level Hardware Description Languages (HCLs), the automatic generation of these micro-architecture models and, more specifically, the pipeline models are promoted. We propose a workflow that aims to automatically construct pipeline datapath models from processor designs described in HCLs. Our workflow is based on the Chis-el/FIRRTL Hardware Compiler Framework. We build at the intermediate representation level the datapath pipeline models. Our work intends to prove the timing properties, such as the timing predictability-related properties. We rely on the formal verification as our method. The generated models are then translated into formal models and integrated into an existing model checking-based procedure for detecting timing anomalies. We use TLA+ modeling and verification language and experiment with our analysis with several open-source RISC-V processors. Finally, we advance the studies by evaluating the impact of automatic generation through a series of synthetic benchmarks.

Listing 2 . 1 -

 21 Parameterization in Chisel. class DecoupledIO [T <: Data](gen: T) extends Bundle { val ready = Input(Bool()) val valid = Output(Bool()) val bits = Output(gen) } class ValidIO [T <: Data](gen: T) extends Bundle { val valid = Output(Bool()) val bits = Output(gen) }

1

  import chisel3.Data ... class Adder[T <: Data](genIn: T, genOut: T) extends Module { val io = IO(new Bundle { val a = Input(genIn) val b = Input(genIn) val out = Output(genOut) := io.a + io.b 11

Figure 2 . 1 -

 21 Figure 2.1 -Chisel/FIRRTL hardware compilation framework. ends tailored for simulators, FPGAs, or ASIC technology processes.Figure2.2 describes the Chisel/FIRRTL compiler framework, where the Chisel design is compiled into FIRRTL representations through simplification transformations. Simplification transformations take a FIRRTL circuit and simplify it to a lower form. First, Chisel is compiled into FIRRTL high form through various passes, which generally check and resolve the high form constructions,

Figure 2 .

 2 2 describes the Chisel/FIRRTL compiler framework, where the Chisel design is compiled into FIRRTL representations through simplification transformations. Simplification transformations take a FIRRTL circuit and simplify it to a lower form. First, Chisel is compiled into FIRRTL high form through various passes, which generally check and resolve the high form constructions, for instance, the CheckTypes and CheckWidths passes, where the types and components widths must be checked to verify the coherence between Chisel constructs. The InferBinaryPoints pass verifies the type match in the assignment constructs. Furthermore, for all circuit components declared with unspecified width or precision, the FIRRTL compiler, through the InferWidths pass, will attempt to infer the strictest possible width value out of all possible values of its incoming connections.

Figure 2 . 2 -

 22 Figure 2.2 -Transformations and passes in Chisel/FIRRTL framework.

Listing 2 . 4 -

 24 Simple pass in Chisel/FIRRTL compiler framework. 1 ... 2 def walkMod(m: DefModule): DefModule = { m.map(walkStmt) } 3 def walkStmt(s: Statement): Statement = { 4 def fct(regNames: mutable[String])(s: Statement): Statement= 5 s match { 6 case r: DefRegister => regNames += r.name; r 7 case _ => s map fct(regNames)

  .3, are: • Instruction Fetch (IF): In this stage, an instruction is read from the instruction memory. The address of memory is contained in the program counter. The fetch stage is the first stage to initiate the instructions traversal of the pipeline. We can notice that the instruction may be retrieved from the memory or directly from the instruction cache. • Instruction Decode (ID): In this stage, an instruction is decoded, and control signals and combinatorial logic are used for the opcode and operands according to each instruction type. • Execute (EX): The ALU (arithmetic logic unit) operations are performed at this stage. It takes the two operands to perform the ALU operation. In this stage, the branch target can also be computed. • Memory Access (MEM): In this stage, the memory accesses are performed with read and write to/from memory instructions. The stage is also responsible for stalls due to cache misses. • Write-Back (WB): In this stage, the computed value is written back to the register file. It writes the results of the arithmetic operations or the data read from memory.

Figure 2 . 3 -

 23 Figure 2.3 -Classical 5-stage pipeline with forwarding.

Figure 2 .

 2 5 describes the Rocket

Figure 2 . 4 -

 24 Figure 2.4 -Pipeline diagram of Sodor 5-stage, from [1]. core pipeline.

Figure 2 . 5 -

 25 Figure 2.5 -Rocket Core pipeline, from [2].

Figure 2 . 6 -

 26 Figure 2.6 -Fetch, Pcgen stages of Rocket core pipeline, from [2]

Figure 2 . 7 -

 27 Figure 2.7 -Four stages of Rocket core pipeline, from [2].

Figure 3 . 1 -

 31 Figure 3.1 -Structure of a VHDL-based static analysis framework, from [3].

Figure 3 . 2 -

 32 Figure 3.2 -VHDL timing model abstractions, from [4].

1

  <processor class="otawa::hard::Processor"> 2 ...

Figure 3 . 3 -

 33 Figure 3.3 -Chronos pipeline modeling overview.

Figure 3 . 4 -

 34 Figure 3.4 -A control flow graph and its control dependence subgraph, from [5].

Figure 4 . 1 -

 41 Figure 4.1 -Formal verification of timing properties from hardware designs workflow.

7 .

 7 is defined as follows, in Listing 4.1. Listing 4.1 -Module in Chisel language. 1 class DatPath(width: Int) extends Module { 2 val io = IO (new DpathIo ()) 3 val if_pc_next = Wire (()) 4 val if_reg_pc = RegInit (io.reset_vector) 5 val mem_reg_inst = Reg(UInt()) 6 val wb_reg_inst = Reg(UInt()) width: Int) extends Module { val io = IO(new CoreIo()) val d = Module(new DatPath()) d.io.reset_vector := io.reset_vector }

.

  Each module defines an interface IO to hardware components called a port. A port is simply any data object that has directions assigned to its members. The Chisel module DatPath of RISC-V Sodor processor defines a new type DpathIo, in Listing 4.2, lines 1-4, that can be used as an IO interface with ports defined by Input/Output Chisel language constructs. The Chisel language also includes an IO compound named Flipped type. It changes the direction of all fields of its argument. The class DpathIo defines a Flipped type, line 4, in order to include the IO control interface through the class CtlToDatIo, lines 6-8 in Listing 4.2.Other Constructs. A Chisel module features combinational and/or sequential circuitry design elements using design primitives. The operator := executes a mono-directional connection element-wise from right to left, while the operator <> is a bidirectional (i.e., bulk) connection element-wise. Listing 4.4 -Other Constructs in Chisel language. 1 class Rocket(width : Int) extends Module { val ibuf = Module(new IBuf()) ibuf.io.imem <> io.imem.resp when (!ctrl_killd) { ex_reg_pc := ibuf.io.pc } }

Figure 4 . 2 -

 42 Figure 4.2 -FIRRTL Abstract Syntax Tree (AST).

Listing 4 . 5 -

 45 A simple Chisel code. 1 val reg1 = RegInit(0.U(4.W)) 2 val reg2 = RegInit(0.U(4.W)) 3 reg1 := value 4 when (cond) { reg2 := reg1 } Listings 4.6 and 4.7 describe, respectively, the FIRRTL high form and low form obtained from the Chisel code presented in Listing 4.5. Listing 4.6 -FIRRTL high form from Listing 4.5. 1 reg reg1 : UInt<4> , clock with : reset => (reset, UInt<4> ) reg reg2 : UInt<4> , clock with : reset => (reset, UInt<4> ) reg1 <= value when cond : reg2 <= reg1 Listing 4.7 -FIRRTL low form from Listing 4.5. 1 reg reg1 : UInt<4> , clock with : reset => (UInt<1> , reg1) reg reg2 : UInt<4> , clock with : reset => (UInt<1> , reg2) node _GEN_0 = mux(cond, reg1, reg2) reg1 <= mux(reset, UInt<4> , value) reg2 <= mux(reset, UInt<4> , _GEN_0)

Listing 4 . 8 -

 48 Chisel code of Kyogen processor. 1 val imem_read_sig: Bool = RegInit(false.B) val imem_req: Bool = RegInit(false.B) when (cond) { imem_req := RegNext(imem_read_sig) } Bulk Connection Compilation. The bidirectional connection is performed using the bulk connection constructor provided by the Chisel language. It is expressed by the operator <> and allows components with aggregate types Listing 4.9 -FIRRTL high form from Listing 4.8. reg imem_read_sig : UInt<1> , clock with : reset => (reset, UInt<1> ("h0")) reg imem_req : UInt<1> , clock with : reset => (reset, UInt<1> ("h0")) when cond: reg REG_1 : UInt<1> , clock with : reset => (UInt<1> ("h0"), REG_1) REG_1 <= imem_read_sig imem_req <= REG_1 to be connected in a type-safe manner with a single statement. However, the FIRRTL compiler removes this bulk connection through transformations. These passes rewrite the bulk connection into a series of individual connections. To illustrate this feature, we present a snapshot of the Chisel code in Rocket processor in Listing 4.10, and its corresponding FIRRTL code is described in Listing 4.11. Listing 4.10 -Chisel code of Rocket processor class FrontendResp extends Bundle { val pc = UInt(32) val data = UInt(40) } class IBuf extends Module { val io = IO(new Bundle { val imem = Flipped(Decoupled(new FrontendResp)) ..... })} class FrontendIO extends Bundle { val resp = Flipped(Decoupled(new FrontendResp))} class Rocket extends Module { val io = IO(new Bundle { val imem = new FrontendIO .....}) val ex_reg_pc = Reg (size) val ibuf = Module (new IBuf) when (cond1) { ex_reg_pc := ibuf.io.pc } ibuf.io.imem <> io.imem.resp } 1 module IBuf: output io: flip imem: {flip ready: UInt<1>, valid: UInt<1>, bits: {pc: UInt<40>, data: UInt<32>} module Rocket: output io: imem: flip resp: {flip ready: UInt<1>, valid: UInt<1>, bits: {pc : UInt<40>, data: UInt<32>}} inst ibuf of IBuf 10 when cond1: 11 ex_reg_pc <=ibuf.io.pc 12 ibuf.io.imem.bits.pc <=io.imem.resp.bits.pc 13 ibuf.io.imem.bits.data <=io.imem.resp.bits.data The Rocket module includes the module IBuf, in Listing 4.11, line 9, using the instance element inst. Each module has its IO interface grouped in Bundle type, in Listing 4.10, lines 5, and 12. Each field is a simple input/output or an instance of another defined IO class. For Rocket module, the value imem is an IO instantiated from the class FrontendIO and then FrontendResp, line 6. This IO implementation is performed through the compound type of the IO interface named DecoupledIO. DecoupledIO is an interface for data transfer. It has three signals or elements: valid and bits are output signals controlled by the source, the first is activated if there is data to transfer and the second corresponds to the data. ready is an input signal controlled by the receiver and indicates that it is ready to receive the data. For the modules Rocket and IBuf, the class FrondendResp, lines 1-3, is an IO interface used as DecoupledIO, lines 6, 13, and 10. In order to connect the IO interface of two modules, the bulk-connection <> is implemented in the module Rocket. This connection is shown with red arrows in Listing 4.10, line 19. The connections of this operator are then compiled into individual connections of each construction field, in lines 12-13 in Listing 4.11. Each individual field pc and data in Rocket and IBuf modules are

  Pipeline. The pipeline design in the Kyogen processor is presented as a 5-stage (IF, ID, EX, MEM, WB) with a mono-module architecture. Its pipeline architecture is presented in a single Chisel/FIRRTL module as shown in Figure 6.7.

1 10 ex_pcFigure 4 . 3 -Figure 4 . 4 -

 104344 Figure 4.3 -Datapath pipeline module of Kyogen processor.

Listing 4 . 13 -

 413 Simplified Chisel code of Rocket datapath pipeline. class RocketTile: val core = Module(new Rocket) frontend.module.io.cpu <> core.io.imem ----------------class Rocket: val ex_reg_pc = Reg (size) /* decls: mem_reg_pc and wb_reg_pc */ val ibuf = Module (new IBuf) when (cond1) { ex_reg_pc := ibuf.io.pc /* updates: mem_reg_pc and wb_reg_pc */ } ibuf.io.imem <> io.imem.resp----------------class Frontend: val io = IO(... /* cpu field */) /* decls: s1_pc and s2_pc */ s2_pc := s1_pc val fq = Module (new ShiftQueue) fq.io.enq.bits.pc := s2_pc io.cpu.resp <> fq.io.deq----------------class IBuf: val io = new Bundle {/* imem and pc fields */} val buf = Reg (io.imem.bits) buf.pc := io.imem.bits.pc io.pc := Mux (cond2, buf.pc, io.imem.bits.pc) ----------------class ShiftQueue : io.deq.bits := io.enq.bits Listing 4.14 -High-form FIRRTL for Listing 4.13.

Figure 4 . 5 - 5 Array (C1 → exe_alu_out, 6 C2 → mem_wbdata, 7 C3

 45567 Figure 4.5 -Datapath pipeline modules of Fuxi.

1

  def forwardReg(read: RegReadIO, rf: RegReadIO) { /* C1-C3 : condition signals */ when (C1) { read.data := io.aluReg.data } . elsewhen (C2) { read.data := io.memReg.data } . elsewhen (C3) { read.data := io.wbReg.data } . otherwise { 10 read.data := rf.data 11 } 12 } 13 forwardReg(io.regRead1, io.rf1) 14 forwardReg(io.regRead2, io.rf2) Listing 4.18 -FIRRTL high form of forwarding implementation in the pipeline of Fuxi. 1 node _T = neq(io.regRead1.addr, UInt<1> ("h00")) node _T_1 = and(io.regRead1.en, _T) when _T_1 : node _T_2 = eq(io.regRead1.addr, io.aluReg.addr) node _T_3 = and(io.aluReg.en, _T_2)

Definition 13

 13 For a register r ∈ Regs M , we denote by C r the register context of r, defined by the pair ⟨In r , out⟩ with In r and out being the input frontier and the output connection of r respectively. The register context C r is computed by an operator regs_ctx : AST M × Regs × I/Os → In × Regs where In is the set from Definition 12.

Definition 14

 14 For an output port p ∈ I/Os M , we denote by Out p the output frontier of p, defined by {c 1 , c 2 , ..c i .., c n }, where c i ∈ Regs M or c i ∈ I/Os M . An output frontier is established for each output port p of a module M which registers or input ports are connected to it. The connections between the module's registers and the output port are particularly important when connecting registers from different modules. Definition 15 For an output port p ∈ I/Os, we denote by C io the output context of p, defined by (Out p , p) with Out p and p being the output frontier and the output respectively. The output context C io is computed by an operator ios_ctx : AST M × Regs × I/Os → Out × I/Os where Out is the set from Definition 14.

Definition 18 Algorithm 2 :2 foreach m ∈ o do 3 ( 4 C 5 C

 182345 This graph is generated by an operator preced_regs : Cr × Cio → I where Cr and Cio are the sets in Definition 13 and Definition 15 respectively whereas I is the graph from Definition 16. The operator ctx_reg : Regs → 2 Regs is defined as ctx_reg(r) = R where for each r i ∈ R, ∃ctx ∈ Ctxs with ctx = cond → U pds and r, r i ∈ U pds. ctx_reg places registers from different connected components of IR P . Pipeline datapath construction: Register Analysis Input : P and AST P = {AST 1 , ..., AST n } Output: Regs → Stages -pipeline datapath of P 1 o ← order_mods(P, AST p ) /* order modules based on instancing, ⊤ is last. */ I/Os m , Regs m , Ctxs m ) ← process_mod(AST m ) r ← C r ∪ regs_ctx(AST m , Regs m , I/Os m ) io ← C io ∪ ios_ctx(AST m , Regs m , I/Os m )the processing order of the pipeline modules is determined, in line 1, the algorithm calculates a module summary, in lines 4-5, for each module of P. The intra-module phase constructs the register context for the relevant module, in line 4. The inter-module phase performs with the output context constructed, in line 5. The last iteration, which is over the top ⊤ module, is followed by the construction of the intermediate representation of P, in line 6, used to generate the pipeline datapath.

  ...... ......... ......... ......... ......... output op2 ......... ......... ......... .........

Figure 5 . 1 -Figure 5 . 3 -

 5153 Figure 5.1 -Register analysis for mono-module datapath pipeline design.

Figure 5 .

 5 Figure 5.4 represents the context of all the registers described in these examples above. Now, we illustrate the Algorithm 1 application on the RISC-V Mini processor in Figure 5.5. RISC-V Mini processor is mono-module datapath pipeline

Figure 5 . 4 -Figure 5 . 5 -

 5455 Figure 5.4 -RISC-V Mini registers context.fe_inst, we go through the AST with walkStatement first to get the wire inst, which is a multiplexer Mux and corresponds to an expression node in FIRRTL. Then, we stop at io.ctrl.inst_kill as the input frontier through multiple walkExpression calls.

Figure 5 . 6 -Example 7 Example 8

 5678 Figure 5.6 -Register analysis for multi-module datapath pipeline design

Figure 5 . 7 -

 57 Figure 5.7 -Outputs context in RISC-V Sodor-3stages.

Figure 5 . 91 Reg

 591 Figure 5.8 illustrates how to obtain the connection between registers of these two modules through the Core module IO interface. Now, we illustrate how we construct the intermediate representation of RISC-V Sodor-3 stages pipeline design through the application of the Algorithm 2. For the three pipeline modules of RISC-V Sodor-3stages, order_mods

Figure 5 . 9 -

 59 Figure 5.9 -Intermediate representation graph for RISC-V Sodor 3-stage simplifications. Our evaluation is on a quad-core Intel Core i7 at 1.90GHZ

Algorithm 3 :2 foreach m ∈ o do 3 ( 4 C 5 C

 3345 Pipeline datapath construction Input : P and AST P = {AST 1 , ..., AST n } Output: Regs → Stages -pipeline datapath of P 1 o ← order_mods(P, AST p ) /* order modules based on instancing, ⊤ is last. */ I/Os m , Regs m , Ctxs m ) ← process_mod(AST m ) r ← C r ∪ regs_ctx(AST m , Regs m , I/Os m ) io ← C io ∪ ios_ctx(AST m , Regs m , I/Os m ) 6 IR P ← preced_regs(C r , C io ) /* build intermediate representation of P */ 7 assign_regs(1, P C, IR P , Regs) /* assign registers to stages, PC is in stage 1 */ Algorithm 4 presents the assignment of registers to pipeline stages. The intermediate representation IR P is a non-strongly connected graph that can

Figure 6 .Figure 6 . 1 -

 661 Figure 6.1 illustrates this case in the processor RISC-V Sodor 5-stage. The source registers if_pc, ex_reg1 and ex_reg2 of the register dec_reg are already assigned, and there is no relation between the source register of minimal stage if_pc with the other sources. So, we assign to dec_reg the minimal stage of its sources plus 1.

Algorithm 4 : 2 if 5 else if C1_min then 6 to_stage

 4256 Register to pipeline stage assignment 1 Function assign_regs(i, reg, IR P , Regs): /* C1_* and C2 identify r in IR P */ C1_linear then 3 to_stage(r) = i + 1 ; /* linear_case 1 */ 4 assign_regs(i + 1, r, IR P , Regs) (r) = i + 1 ; /* min_case 1 */ 7 assign_regs(i + 1, r, IR P , Regs) , r ′ ) ← select_reg(IR P , Regs) 16 assign_regs(i ′ , r ′ , IR P , Regs)

Figure 6 . 2 -

 62 Figure 6.2 -Simple application of max case 1 (C1_max).

Listing 6 . 1 -

 61 Simplified code for compressed instructions, in Rocket 1 class Rocket : val ibuf = Module (new IBuf) useCompressed: Boolean = true val fetchWidth: Int = if ( useCompressed) then 2 else 1 ex_reg_pc := ibuf.io.pc

Figure 6 . 3 -

 63 Figure 6.3 -Inaccurate application of min/max_case 1.

Figure 6 . 4 -

 64 Figure 6.4 -Simple application of case 2.

Figure 6 . 5 -

 65 Figure 6.5 -Intermediate representation graph for RISC-V Sodor 5-stage

Figure 6 . 6 -

 66 Figure 6.6 -RISC-V Sodor 5-stage pipeline datapath model.

Listing 6 . 5 ( 6 (

 656 2 presents a subset of the data forwarding implemented from the WB and MEM towards the EX stage. The wire ex_reg_rs1_bypass is updated from the output of the mem_alu_out register (line 5), located in the MEM stage, or from the wb_alu_out register (line 6), located in the WB stage, through the Chisel MuxCase construction. In the FIRRTL low form, a MuxCase is translated into a cascade of multiplexers. This forwarding corresponds to the blues arrows, shown in Figure 6.7, from the registers wb_alu_out and mem_alu_out to the input of the ALU red box. The other blue arrow, between the register wb_reg_waddr and the input of the ALU, is part of the check to detect the need for forwarding a value, as in line 6. Listing 6.2 -Forwarding in KyogenRV 5-stage. 1 val ex_reg_rs1_bypass = Wire(UInt(32.W)) 3 /* Ci, i = 1..2 -conjuncts of write enable and selection → signals */ 4 ex_reg_rs1_bypass := MuxCase(ex_rs(0), Seq( ex_reg_raddr(0) === mem_reg_waddr && C1) → mem_alu_out ex_reg_raddr(0) === wb_reg_waddr && C2) → wb_alu_out)) 7 ... 8 when (C4 /* no stalling condition */) { 9 mem_rs(0) := ex_reg_rs1_bypass 10 } Finally, our algorithm assigns the register pc_cntr with the min_case 2 , where its source registers mem_pc, mem_alu_out are assigned in the same pipeline stage.

Figure 6 . 7 -

 67 Figure 6.7 -Partial representation of the abstract pipeline model of the Kyo-genRV processor.

Figure 6 . 8 -

 68 Figure 6.8 -Partial representation of the abstract pipeline model of the Rocket processor.

2 runtimeFigure 6 . 9 -

 269 Figure 6.9 -Execution of the register assignment algorithm, i.e., Algorithm 4.

Listing 6 . 3 - 1 / 9 / 14 .

 631914 Control registers in KyogenRV processor. * Called in KyogenRVCpu Module */ 10 class KyogenRVCpu extends Module { 11 val ex_ctrl: IntCtrlSigs = RegInit() 12 ex_op1 := MuxCase (0.U(32.W), 13 (ex_ctrl.alu_op1 == OP1_RS1) → ex_reg_rs1_bypass,

  -EXTENDS M1, M2, ... /* add declarations, definitions from the → modules M1, M2 to the current module */ CONSTANTS .../* Constants declaration */ VARIABLES ... /* State variables */ -

Algorithm 5 :

 5 Datapath TLA+ Model Generation Input : IR P , ElmtP rog and P regs = Regs → Stages -pipeline datapath of P Output: InitP ipe, U pdateP ipe -Datapath TLA+ specification of P 1 State_var ← (currCycle, Stages) /* State variables. */ 2 InitP ipe ← formal_Init( P regs, State_var) 3 SrcReg ← MaxCaseRegs (IR P )/* Regs assigned with max case. */ 4 P redRegSel ← FRegsSelection (IR P ) /* Regs used as a selection of combinatorial logic(mux) */ 5 U pdateP ipe ← formal_Next( P regs, State_var, IR P , SrcReg, P redRegSel, ElmtP rog)

Algorithm 6: formal_Init function 1 Function 2 StageInit ← T RU E 3 foreach

 123 formal_Init(P regs, State_var): (Stage i , Regs) ∈ P regs do 4 Stage i _assign = Stage_upd(Stage i , R(Regs, empty)) StageInit = StageInit ∧ Stage i _assign 5 return StageInit;

  insts == [ [type |-> "alu", rd |-> "rd", rs1 |-> "rs1", rs2 |-> "rs2", conds = {cond_1, .../* Conditions of type select_cond */ }], [type |-> "jal", rd |-> "rd", rs1 |-> "empty", rs2 |-> "empty", conds = {cond_2,.../* Conditions of type select_cond */ }], [type |-> "lw", rd |-> "rd", rs1 |-> "rs1", rs2 |-> "empty", conds = {cond_3,... /* Conditions of type select_cond */ }], ...]

Algorithm 8 : 2 stageStall ← T RU E 3 i ← 1 4while i <= MemStage do 5 foreach 7 i = i + 1 8 9 stageStall

 82315719 formal_Stall function 1 Function formal_Stall(P regs, State_var, M emStage, IR P ): Stage i ∈ P regs do 6 stageStall = stageStall ∧ Stage_upd(Stage i , U N CHAN GED) Stage i _assign = Stage_upd(Stage M emStage+1 , R(Regs, empty)) = stageStall ∧ Stage i _assign 10 return stageStall; We integrated the stalling logic into the pipeline definition via a TLA+ operator Stall, which is defined as a conjunction between the pipeline stalling stages and currCycle, delay_cycle variables. stall_delay is incremented until stall_cond becomes false. Stall == ... /\ stall_cond /\ StallPipe /\ stall_delay' = stall_delay + 1 /\ currCycle' = currCycle + 1 The update state Next integrates the pipeline updates without stalling in TransPipe and with the stalling logics in Stall. The pipeline update is defined as follows: TransPipe == ... /\~stall_cond /\ UpdatePipe /\ currCycle' = currCycle + 1 /\ stall_delay' = 0

2 .

 2 The update of this register in stage 4 is as shown: stage_4' = [ ... ex_reg_pc |-> buf_pc ...]

  stage_6' = [ wb_reg_wdata |-> IF cond_1 THEN stage_5.mem_reg_pc ELSE IF cond_2 THEN stage_5.mem_reg_wdata ELSE stage_5.mem_reg_inst ...] We refer to the ISA model of instruction classes to define their execution patterns and to evaluate the corresponding conditions to true. insts == [ [type |-> "add", rd |-> "rd", rs1 |-> "rs1", rs2 |-> "rs2", conds = {cond_2} ], [type |-> "jal", rd |-> "rd", rs1 |-> "empty", rs2 |-> "empty", conds = {cond_1} ], ...]

Figure 7 . 1 -

 71 Figure 7.1 -Example of counter-intuitive timing anomalies

Figure 7 .Figure 7 . 2 -

 772 Figure 7.2 -Timing anomalies intuition, from[START_REF] Asavoae | Formal executable models for automatic detection of timing anomalies[END_REF]

Titre:

  Sémantique Formelle d'une Infrastructure de Compilation Matériel Mots clés: Modélisation des processeurs, Langages de Construction de Matériel (HCLs), Chemin de données du pipeline, Anomalies temporelles, Vérification de modèle

Table 2 .

 2 1 -Syntax and semantic of Chisel constructs.

	Chisel_Constructs	Syntax	Semantics
	Types	Bool(), UInt(), SInt()	Boolean, Unsigned/Signed integers
	Aggregate types	class MyBundle extends Bundle { val a = Bool () val b = UInt ()}	Define Data types indexed by name
		Vec(elts:Iterable[Data])	An indexable vector of Data types
	Operators	!x, x, x + y	Logical NOT, Bitwise NOT, Addition
	Memory	Mem(n:Int, out:Data)	Addressable memory with n as a depth
	Registers	Reg(type)	Create type register
		RegInit()	Register with initialization value
		RegNext()	Register updated every clock cycle
	Wires	val x = UInt()	Allocate wire of type UInt

  2 , A 3 , ....) ∈ (P(AP )) ω } is a linear-time property over AP .

	Definition 11 (invariant). A (linear-time) property is an invariant if there exists

a state predicate φ such that P = {(A 1 , A 2 , A 3 , ...) ∈ (P(AP )) ω |∀i ∈ N * , A i |= φ}. Such a state predicate φ is called an invariant (condition).

  IF-THEN-ELSE and LET-IN to write the local definition.

	Listing 2.5 -Simplified TLA+ specification.
	VARIABLES currCycle, _IF, prog,......
	Init == /\ currCycle = 0
	/\ _IF = [ PC |-> empty ]
	........
	FillIF == LET nxt == next_instr (prog) IN
	/\ _IF' = [ PC |-> IF condFillIF THEN nxt ELSE _IF ]
	/\ currCycle' = currCycle + 1
	........
	Next == FillIF \/ ......
	Spec == Init /\ [][Next]_<< currCycle, _IF, prog,... >>
	Prop == currCycle < 50

Analysis Specification VHDL design Control-Flow Intermediate Representation (CRL2) Program Analyzer Generator (PAG) Static Analysis Analysis Results

  .5. More precisely, each pair of pipeline stages (e.g., Fetch and Decode) is connected through an interface I/O named StageIO, described in a module MidStage.

			Core
	Stage(i)		MidStage		Stage(i+1)
			StageIO
	io.stage (i)	io.prev	ff	io.next	io.stage (i+1)
	reg(i)				reg(i+1)

  illustrate following the examples of input frontier and register context.

Example 4

The register context of fe_inst in Datapath processor, in Listing 5.1 line 15, includes the constructors inst which is a Mux primitive. With a recursive browse of all nodes starting from this register to all inputs frontier, the register context of this register are the pairs <io.ctrl.inst_kill, fe_inst> <io.icache.resp.bits.data, fe_inst>, with module inputs I/Os as input frontiers.

Example 5

The register context of fe_pc, ew_pc, ew_inst in Datapath processor, in Listing 5.1, lines 14, 18, 19 are the pairs <pc, fe_pc>, <fe_pc, ew_pc>, <fe_inst, ew_inst> respectively. All their input frontiers are delimited by processor registers.

Example 6

The register context of ew_alu in Datapath processor, in Listing 5.1, lines 20, is the pair <alu.io.out, ew_alu> with alu.io.out ∈ alu ∈ Exts M , where the input frontier is an element of the external module ALU.

  Frontend, DatPath, and then Core, where Core is the top ⊤ of P Sodor3 . For each module, with the previous order, the AST m is visited through process_mod function developed in Algorithm 1. The algorithm's illustration on a single module is detailed in the previous subsection 5.2.1.

		Core
	FrontEnd		DatPath
		frontend.io.cpu
		<>
	frontend.exe_reg_pc	dpath.io.imem	dpath.wb_reg_pc
	Figure 5.8 -IO interface for register precedence relation
	produces the ordered set

Then we construct the register context for the module DatPath, it includes the pairs <io.imem.resp.bits.pc, wb_reg_pc>, <io.ctl, wb_reg_ctrl>, <io.imem.resp.bits.inst, wb_reg_wbaddr> where their input frontiers are the module inputs. Then, the pair <alu.io.out, wb_reg_alu> with alu.io.out ∈ Exts M , where the input frontier is an element of the external module ALU. The process is also applied for the module FrontEnd to construct the register context and the output context, which includes the pairs <exe_reg_pc, io.cpu.resp.bits.pc>, <exe_reg_inst, io.cpu.resp.bits.inst>. Finally, the process ends with the module Core, which includes the interface IO (frontend.io.cpu <> dpath.io.imem), line 5, in Listing 5.2. This interface implemented in this module allows the registers context delimited by the module inputs to extend to the other module registers, and then obtain the intermediate representation specified in preced_regs function. For example, we can obtain the precedence relation between two registers (dpath.exe_reg_pc, frontend.wb_reg_pc) through the register context <frontend.io.imem.resp.bits.pc, frontend.wb_reg_pc> and the output context <dpath.exe_reg_pc, dpath.io.cpu.resp.bits.pc> which can be reduced to the precedence relation using the interface (frontend.io.cpu <> dpath.io.imem). Then, the intermediate graph (as in Figure

Table 5 .

 5

	1 -Register analysis experimental results on RISC-V processor
	designs.
		LOC #M p #Regs #Cxts #F rt #IRp	Runtime (s)
	Mini	241	1	11	3	8	18	0.12
	Sodor-5	646	1	37	14	88	70	0.68
	KyogenRV 4568	1	108	59	53	128	16.38
	Sodor-3	575	3	26	8	17	24	0.52
	Fuxi	2438	10	54	9	33	78	1752.51
	Rocket	4159	5	240	68	224	133	49.63

Table 6 .

 6 1 -Experimental results on KyogenRV processor.

  -Init == .... /* Initial state predicate */

	Next == \/ Actions /* Next state relation */
	...
	Spec == Init /\ [] [Next]_<<Variables>> /* Specification */
	Prop == ... /* Property to verify */

  .6. As described in formal_Init function in Algorithm 6. The record R defined in Stage i _assign corresponds to the initialization of the stage 3 registers with empty. The initialization for stage_3 is as follows:The TransPipe models the progress of the pipeline where there is no stalling.The operator update_stage_3(regs) stands for the following partial update of stage_3 (i.e., only 2 registers, ex_pc and ex_alu_op1 out of 13 registers

	InitPipe == ... /\ stage_3 = [ ex_pc |-> empty,
	ex_alu_op1 |-> empty,
	ex_alu_op2 |-> empty,
	ex_rs2_data |-> empty ]
	... /\ currCycle = 0
	TransPipe == ..../\~stall_cond
	/\ update_stage_3(regs) /\ ...
	/\ currCycle' = currCycle + 1
	are shown):
	stage_3' = [ ex_pc |-> stage_2.dec_pc,
	ex_alu_op1 |-> IF bypass_3_5 THEN stage_5.wb_wbdata
	ELSE IF bypass_3_4 THEN stage_4.mem_alu_out
	ELSE IF bypass_3_3 THEN stage_3.ex_alu_op2
	ELSE IF cond_1 THEN stage_5.wb_wbaddr
	ELSE IF cond_2 THEN stage_4.mem_wbaddr
	ELSE IF cond_3 THEN stage_2.ex_wbaddr
	ELSE IF cond_4 THEN stage_2.dec_pc
	ELSE stage_2.dec_inst ... ]

Table 7 .

 7 1 -Statistics on TLA+ specification of RISC-V processor designs

		LOC(automatic) LOC(manual) automatic
	Sodor 3-stage	40	16	71%
	RISC-V Mini	55	16	77%
	Sodor 5-stage	145	25	85%
	KyogenRV	239	37	86%
	Rocket	103	25	80%

Table 7 .

 7 2 -Impact of stalling checks on TLA+ pipeline models.

		#Instr	Time (s)	#Instr	Time (s)
	Mini_complete Mini_datpath	100	02 01	200	03 02
	Sodor3_complete Sodor3_datpath	100	02 01	200	03 02
	Sodor5_complete Sodor5_datpath	100	16 13	200	23 18
	Kyogen_complete Kyogen_datpath	100	21 18	200	29 25
	Rocket_complete Rocket_datpath	100	17 15	200	23 17
	Fuxi_complete Fuxi_datpath	100	17 10	200	26 18

Table 7 .

 7 3 -Experimental results for the absence of timing anomalies for RISC-V Sodor processor.

		#Regs #Instr #Execs	Time (s)	Diam -eter	States F ound
	simple sodor_subset	5 11	200	65536	32 40	1170 801678
	sodor_complete 37			54

Table 7 .

 7 [START_REF]Semi-automatic derivation of timing models for WCET analysis[END_REF] -Experimental results for the absence of timing anomalies for Rocket processor.

		#Regs #Instr #Execs	Time (s)	Diam -eter	States F ound
	simple rocket_subset	6 16	200	65536	38 46	1172 801707
	rocket_complete 30			59

Table 7 .

 7 5 -Experimental results for timing anomalies detection with multiple program depth for Sodor 5-stage processor.

		#Regs #Ins #Exc	Time (m : s)	Diam -eter	States F ound
	simple sodor_subset	5 11	40	1024	00:24 00:27	172	83288
	sodor_complete 37			00:45
	simple sodor_subset	5 11	80	1024	01:09 01:23	332 167768
	sodor_complete 37			01:54
	simple sodor_subset	5 11	120	1024	01:29 02:01	492 252248
	sodor_complete 37			02:51
	simple sodor_subset	5 11	160	1024	01:45 02:07	652 336728
	sodor_complete 37			02:59
	simple sodor_subset	5 11	200	1024	01:57 02:20	812	421208
	sodor_complete 37			03:10

Table 7 .

 7 6 -Experimental results for timing anomalies detection with multiple program depth for Rocket processor.

		#Regs #Ins #Exc	Time (m : s)	Diam -eter	States F ound
	simple rocket_subset	6 16	40	1024	00:02 00:03	174	83321
	rocket_complete 30			00:04
	simple rocket_subset	6 16	80	1024	00:05 334 167801 00:17
	rocket_complete 30			00:27
	simple rocket_subset	6 16	120	1024	00:09 494 252281 00:42
	rocket_complete 30			00:52
	simple rocket_subset	6 16	160	1024	00:14 654 336761 01:30
	rocket_complete 30			01:45
	simple rocket_subset	6 16	200	1024	00:28 01:50	814	421241
	rocket_complete 30			02:05

Table 7 .

 7 7 -Experimental results for timing anomalies detection with multiples latencies for Sodor 5-stage processor.

		#Regs #Ins	#Exc	Time (m : s)	Diam -eter	States F ound
	simple sodor_subset	5 11	200	1024	00:09 832 00:10	125999
	sodor_complete 37			00:13
	simple sodor_subset	5 11	200	16384	04:43 832 3200254 05:50
	sodor_complete 37			07:45
	simple sodor_subset	5 11	200	262144	15:36 17:30	832	7614589
	sodor_complete 37			22:40
	simple sodor_subset	5 11	200	4194304	35:49 832 16921893 41:27
	sodor_complete 37			45:15

Table 7 .

 7 8 -Experimental results for timing anomalies detection with multiples latencies for Rocket processor.

		#Regs #Ins	#Exc	Time (m : s)	Diam -eter	States F ound
	simple rocket_subset	6 16	200	1024	00:08 834 00:09	98927
	rocket_complete 30			00:11
	simple rocket_subset	6 16	200	16384	02:49 834 3200343 03:13
	rocket_complete 30			03:40
	simple rocket_subset	6 16	200	262144	19:15 22:10	834 7614726
	rocket_complete 30			24:19
	simple rocket_subset	6 16	200	4194304	47:37 834 16922102 53:36
	rocket_complete 30			58:13

Table 7 .

 7 [START_REF] Ballabriga | OTAWA: an open toolbox for adaptive WCET analysis[END_REF] -Experimental results for timing anomalies detection with various processor designs.

		#Regs #Ins #Execs	Time (m : s)	Diam -eter	States F ound
	RISC-V Mini sodor 3stage	11 8	200	4194304	18:38 21:07	828 16710594 828 16710594
	sodor 5stage	37			45:15	832 16921893
	Kyogen	74			53:18	832 16921893
	Rocket	30			58:13 834 16922102
	Fuxi	53			48:05 832 16921893

https://github.com/riscvarchive/riscv-cores-list

IR P ← preced_regs(C r , C io ) /* build intermediate representation of P */ Algorithm 2 constructs a pipeline datapath out of a given set of pipeline modules P while working on the corresponding AST P representation. Once

return to_stage;

return StageU pdate;

Registers. In Chisel, there are several ways to declare and specify the connection to the register input. As shown in RISC-V Sodor processor in Listing 4.1, the variable if_reg_pc is a register declared in the module DatPath using the primitive RegInit, initialized with a value io.reset_vector, line 4, and updated then in when construction that defines a conditional block, C1, line 8. Therefore, we pass the next value to the register wb_reg_inst using the primitive RegNext, it will clock the new value every cycle unconditionally, line 11. Note that UInt design unsigned Int type for the registers mem_reg_inst, wb_reg_inst, lines 5-6.