{"id":5276,"date":"2025-10-08T15:37:32","date_gmt":"2025-10-08T13:37:32","guid":{"rendered":"https:\/\/pepr-cloud.fr\/fr\/?page_id=5276"},"modified":"2025-10-21T14:36:14","modified_gmt":"2025-10-21T12:36:14","slug":"conception-rigoureuse-de-circuits-basee-sur-les-methodes-formelles","status":"publish","type":"page","link":"https:\/\/pepr-cloud.fr\/fr\/conception-rigoureuse-de-circuits-basee-sur-les-methodes-formelles\/","title":{"rendered":"Conception rigoureuse de circuits bas\u00e9e sur les m\u00e9thodes formelles"},"content":{"rendered":"
\"\"<\/span>
\n

<\/p>\n<\/div><\/div>\n\n\n\n

<\/div>\n\n\n\n

Conception rigoureuse de circuits bas\u00e9e sur les m\u00e9thodes formelles<\/strong><\/h2>\n\n\n\n
<\/div>\n\n\n\n
\n
\n
\"\"<\/figure><\/div><\/div>\n\n\n\n
\n

Zachary ASSOUMANI <\/strong>
D\u00e9but<\/strong> : 01\/10\/2024
Fin<\/strong> : 01\/10\/2027
Laboratoire<\/strong> : CONVECS
Projet<\/strong> : Archi-CESAM<\/a>
Mots-Cl\u00e9s<\/strong> : M\u00e9thodes formelles\u00a0; Architecture mat\u00e9rielle\u00a0; Cloud computing<\/em>
Type de contrat<\/strong> : Doctorat<\/strong><\/mark><\/kbd><\/p>\n<\/div>\n<\/div>\n\n\n\n

<\/div>\n\n\n\n

Pr\u00e9sentation du sujet <\/strong><\/h1>\n\n\n\n
<\/div>\n\n\n\n

Dans un premier temps, le travail consistera \u00e0 \u00e9tudier HPDcache, un cache de donn\u00e9es L1 hautes performances compatible avec les processeurs RISC-V. HPDcache est utilis\u00e9 dans l’impl\u00e9mentation CVA6 du RISC-V utilis\u00e9 par plusieurs industriels. Il s’agit d’un cache hautement configurable, avec ex\u00e9cution dans le d\u00e9sordre (out-of-order) et reex\u00e9cution (replay), muni d’interfaces compatibles avec AMBA AXI5 et RISC-V. L’\u00e9tude du HPDcache sera faite en construisant un mod\u00e8le formel de son architecture, qui comporte un pipeline \u00e0 trois \u00e9tages, permettant de traiter environ 10 transactions simultan\u00e9es. Plusieurs configurations seront consid\u00e9r\u00e9es, en fonction des diff\u00e9rentes fonctionnalit\u00e9s activ\u00e9es du HPDcache. Ce mod\u00e8le formel servira de base pour v\u00e9rifier des propri\u00e9t\u00e9s de correction (absence de livelocks et de deadlocks, respect du mod\u00e8le de coh\u00e9rence du processeur, etc.), pour g\u00e9n\u00e9rer des tests de conformit\u00e9 et pour estimer les performances du cache. Dans un deuxi\u00e8me temps, le travail consistera \u00e0 proposer des extensions de la m\u00e9thodologie de conception des circuits avec des m\u00e9thodes formelles (mod\u00e9lisation, v\u00e9rification, test de conformit\u00e9), notamment en consid\u00e9rant les architectures \u00e0 composants communicants (chiplets). Une partie int\u00e9ressante de cette m\u00e9thodologie pourrait \u00eatre des passerelles entre les langages de description de ces circuits et de leurs protocoles de communication sous-jacents et les langages formels utilis\u00e9s pour la v\u00e9rification.<\/p>","protected":false},"excerpt":{"rendered":"

Conception rigoureuse de circuits bas\u00e9e sur les m\u00e9thodes formelles Zachary ASSOUMANI D\u00e9but : 01\/10\/2024Fin : 01\/10\/2027Laboratoire : CONVECSProjet : Archi-CESAMMots-Cl\u00e9s : M\u00e9thodes formelles\u00a0; Architecture mat\u00e9rielle\u00a0; Cloud computingType de contrat : Doctorat Pr\u00e9sentation du sujet Dans un premier temps, le travail consistera \u00e0 \u00e9tudier HPDcache, un cache de donn\u00e9es L1 hautes\u2026<\/p>\n

Continuer la lecture<\/span><\/i><\/a> <\/p>\n","protected":false},"author":2468,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_mc_calendar":[],"footnotes":""},"class_list":["post-5276","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/pages\/5276","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/users\/2468"}],"replies":[{"embeddable":true,"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/comments?post=5276"}],"version-history":[{"count":32,"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/pages\/5276\/revisions"}],"predecessor-version":[{"id":5655,"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/pages\/5276\/revisions\/5655"}],"wp:attachment":[{"href":"https:\/\/pepr-cloud.fr\/fr\/wp-json\/wp\/v2\/media?parent=5276"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}