An effective environment to generate test programs for pipelined processors resorting to formal techniques
External reference persons Nikolaos Deligiannis
Research Groups DAUIN - GR-05 - ELECTRONIC CAD & RELIABILITY GROUP - CAD
Description Formal techniques are a promising approach able to face problems corresponding to the identification of a possible set of input values able to satisfy a given property by a Boolean formula. Many engineering problems can be represented as a set of Boolean expressions, and formal techniques can be used to effectively solve them. In the recent past, some advancements in the state-of-the-art of these techniques, and the availability of more powerful computing systems allowed formal techniques to be used for the solutions of some interesting problems on pipelined processors, such as generating a test program able to detect a fault in the CPU hardware, or maximize the switching activity in a given module of the CPU. The CAD Group working in the Dept. of Control and Computer Engineering works from several years on these topics in cooperation with the University of Friburg in Germany.
Students working on this project will use the FriTest environment developed by the University of Friburg, allowing the user to exploit the power of a state-of-the-art SAT solver for solving problems related to processors. Their task will be to
1) customize the environment so that it can effectively work on a RISC-V processor, facing one of the above problems (i.e., generating a program able to detect a fault, maximizing the Switching Activity in a CPU module, identifying safe faults)
2) run experiments aiming at understanding the advantages and limitations of the environment
3) develop optimized solutions able to widen the capabilities of the environment.
Required skills This proposal is suitable for students enrolled in Computer Engineering. Students from other other curricula will be evaluated case by case.
Deadline 16/01/2024 PROPONI LA TUA CANDIDATURA