As a member of a multidisciplinary technological research team comprised of experts in software/hardware analyses through the application of formal methods, you will actively contribute to a national research project dedicated to the development of a predictability toolbox. This toolbox aims to analyze the worst-case temporal behavior of microarchitectures associated with embedded RISC-V processors. These microarchitectures are generated by a flow from a partner that automatically infers synthesizable Register Transfer Level (RTL) representations of processors from their Instruction Set Architecture (ISA). Your involvement in this project will facilitate the creation of a predictability toolbox that streamlines the exploration of design trade-offs, ultimately leading to the production of highly tailored RISC-V processors designed for Internet of Things (IoT) applications and embedded platforms used in safety-critical systems. A key aspect of predictability analysis involves assessing the worst-case execution time (WCET) of a processor by examining how a given binary code progresses through successive pipeline stages.Timing Anomalies (TAs) are execution phenomena known to hinder these analyses and must be supported. Your main responsibilities will include: Proposing and developing an approach to generate formal models of processor pipelines. This involves utilizing a cycle-accurate intermediate representation of pipelines incorporating their micro-architecture optimizations. While LECA has previously developed formal models of pipelines for TA detection within code, these models were manually created. Utilizing the formally generated models as part of a pipeline analysis in a static WCET analysis tool provided by a collaborative partner. Specifically, the outcomes of cache analyses will guide the identification of temporal variations to be considered in the detection of TAs within basic blocks of input code. Defining microarchitectural-level instructions to alleviate the presence of various types of TAs at basic-block boundaries. These instructions will play a crucial role in the exploration process of RISC-V embedded microarchitectures, particularly when targeting safety-critical systems. You are also expected to : Communicate about the work to the project partners, but also work directly with the French partners of the project; Participate in the scientific dissemination of the team's research results (contributions to publications in international conferences) and in the development of our innovations (writing of patents). To carry out your mission, you will benefit from a first class environment at CEA LIST with access to a large number of reference tools and a strong experience in the application of formal methods to the verification of properties such as temporal anomalies.

Job description: As a member of a multidisciplinary technological research team comprised of experts in software/hardware analyses through the application of formal methods, you will actively contribute to a national research project dedicated to the development of a predictability toolbox. This toolbox aims to analyze the worst-case temporal behavior of microarchitectures associated with embedded RISC-V processors. These microarchitectures are generated by a flow from a partner that automatically infers synthesizable Register Transfer Level (RTL) representations of processors from their Instruction Set Architecture (ISA). Your involvement in this project will facilitate the creation of a predictability toolbox that streamlines the exploration of design trade-offs, ultimately leading to the production of highly tailored RISC-V processors designed for Internet of Things (IoT) applications and embedded platforms used in safety-critical systems. A key aspect of predictability analysis involves assessing the worst-case execution time (WCET) of a processor by examining how a given binary code progresses through successive pipeline stages.Timing Anomalies (TAs) are execution phenomena known to hinder these analyses and must be supported. Your main responsibilities will include: Proposing and developing an approach to generate formal models of processor pipelines. This involves utilizing a cycle-accurate intermediate representation of pipelines incorporating their micro-architecture optimizations. While LECA has previously developed formal models of pipelines for TA detection within code, these models were manually created. Utilizing the formally generated models as part of a pipeline analysis in a static WCET analysis tool provided by a collaborative partner. Specifically, the outcomes of cache analyses will guide the identification of temporal variations to be considered in the detection of TAs within basic blocks of input code. Defining microarchitectural-level instructions to alleviate the presence of various types of TAs at basic-block boundaries. These instructions will play a crucial role in the exploration process of RISC-V embedded microarchitectures, particularly when targeting safety-critical systems. You are also expected to : Communicate about the work to the project partners, but also work directly with the French partners of the project; Participate in the scientific dissemination of the team's research results (contributions to publications in international conferences) and in the development of our innovations (writing of patents). To carry out your mission, you will benefit from a first class environment at CEA LIST with access to a large number of reference tools and a strong experience in the application of formal methods to the verification of properties such as temporal anomalies.

Languages: English Fluent,French Intermediate