Comment je suis arrivé à la spécification formelle d'un processeur RISC-V en F #

Les soirs d'hiver langoureux, lorsque le soleil passait paresseusement à travers le voile des jours, j'ai trouvé la force de m'attaquer à la réalisation d'un rêve de longue date: comprendre comment fonctionnent les processeurs. Ce rêve m'a amené à écrire une spécification formelle de processeur RISC-V. Projet Github


image


Comment c'était


J'avais un tel désir il y a longtemps, quand il y a 20 ans j'ai commencé à m'engager dans mes premiers projets. Il s'agissait pour la plupart de recherches scientifiques, de modélisation mathématique dans le cadre d'articles à terme et d'articles scientifiques. Ce furent les jours de Pascal et Delphi. Cependant, même alors, Haskell et la programmation fonctionnelle ont attiré mon intérêt. Le temps a passé, les langues des projets et des technologies dans lesquelles j'ai été impliqué ont changé. Mais depuis lors, l'intérêt pour les langages de programmation fonctionnels a été un fil conducteur, et ils sont devenus: Haskell, Idris, Agda. Récemment, cependant, mes projets ont été à Rust. Une immersion plus profonde dans Rust m'a amené à étudier les appareils embarqués.


De la rouille à l'embarqué


Les capacités de Rust sont si étendues et la communauté est si active que le développement intégré a commencé à prendre en charge une large gamme d'appareils. Et c'était ma première étape vers une compréhension de niveau inférieur des processeurs.


Ma première carte était: STM32F407VET6 . C'était une immersion dans le monde des microcontrôleurs, dont à cette époque j'étais très loin, et je comprenais assez bien comment le travail se faisait à bas niveau.


Peu à peu, des cartes esp32 , ATmega328 (représentées par la carte Ukraino UNO ) ont été ajoutées ici. L'immersion dans stm32 s'est avérée assez douloureuse - les informations sont nombreuses et souvent pas celles dont j'ai besoin. Et il s'est avéré que développer, par exemple, sur Assembler est une tâche plutôt routinière et ingrate, avec leur sous-ensemble de plus de 1000 instructions. Cependant, Rust a géré cela joyeusement, bien qu'il y ait parfois eu des difficultés d'intégration pour des cartes chinoises spécifiques.


L'architecture AVR s'est avérée nettement plus simple et plus transparente. Les manuels abondants m'ont permis de comprendre suffisamment comment travailler avec un ensemble d'instructions assez limité, et néanmoins de pouvoir créer des solutions très intéressantes. Néanmoins, le chemin Arduino ne m'a pas du tout plu, mais écrire en Asm / C / Rust s'est avéré être beaucoup plus intéressant.


Où est le RISC-V?


Et à ce moment, une question logique se pose - où est le processeur RISC-V ?
C'est la nature minimaliste de l'AVR et sa documentation suffisante qui m'ont ramené à mon rêve précédent pour comprendre comment fonctionne le processeur. À cette époque, j'avais une carte FPGA et les premières implémentations sous forme d'interaction avec des périphériques VGA, de sortie graphique, d'interaction avec des périphériques.


Les livres ont été mes guides pour l'architecture de processeur:


  • John L. Hennessy et David A. Patterson - Architecture informatique: une approche quantitative (La série Morgan Kaufmann en architecture et conception informatique)
  • John L. Hennessy et David A. Patterson - Organisation et conception informatique. L'interface matérielle / logicielle: édition RISC-V
  • David M. Harris et Sarah L. Harris - Circuits numériques et architecture informatique
  • Manuel d'instructions RISC-V

Pourquoi est-ce nécessaire


Il semblerait - tout a déjà été écrit et mis en œuvre depuis longtemps.



diverses implémentations en HDL et langages de programmation. Soit dit en passant, une implémentation assez intéressante de RISC-V sur Rust .


Cependant, ce qui pourrait être plus intéressant que de le découvrir vous-même et de créer le vôtre. Votre vélo ? Ou contribuer à la construction de vélos ? En plus d'un intérêt personnel profond, j'avais une idée - comment essayer de vulgariser, d'intéresser. Et trouvez votre forme, votre approche. Et cela signifie présenter la documentation ISA RISC-V plutôt ennuyeuse sous la forme d'une spécification officielle sous une forme différente. Et il me semble que la voie de la formalisation en ce sens est assez intéressante.


Qu'est-ce que j'entends par formalisation? Un concept assez large. Représentation d'un ensemble de données spécifique sous une forme formelle. Dans ce cas, à travers une description des structures et une description fonctionnelle. Et dans ce sens, les langages de programmation fonctionnels ont leur propre charme. En outre, la tâche est qu'une personne qui n'est pas très immergée dans la programmation peut lire le code comme une spécification, si possible en comprenant le moins possible les spécificités du langage dans lequel il est décrit.
Une approche déclarative, pour ainsi dire. Il y a une déclaration, mais comment cela fonctionne exactement n'est plus essentiel. L'essentiel est la lisibilité, la visibilité et bien sûr l'exactitude. Correspondance des déclarations formelles avec le sens qu'elles contiennent.
image
Total - Je suis vraiment curieux de transmettre mon intérêt aux autres. Il y a une certaine illusion que l'intérêt est le moteur des actions. À travers lequel l'individualité devient et se manifeste. Et cela fait partie de la réalisation de soi, l'incarnation de la créativité.
Ambitieux et un peu de paroles. Et ensuite?


Implémentations existantes


Ils existent et sont actuellement agrégés par le projet: RISC-V Formal Verification .
Liste des spécifications formelles (y compris mon travail): https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md


Comme vous pouvez le voir - ce sont pour la plupart des formalisations en langage Haskell. C'était le point de départ dans le choix d'un langage fonctionnel différent. Et mon choix s'est porté sur F # .


Pourquoi F#


Il se trouve que je connais F # depuis longtemps, mais d'une manière ou d'une autre dans l'agitation de la vie quotidienne, je n'ai pas eu l'occasion de mieux me connaître. Un autre facteur était la plate-forme .NET . Compte tenu du fait que je suis sous Linux, pendant longtemps je n'étais pas satisfait de l'IDE, et le mono semblait assez brut. Et revenir à Windows juste pour MS Visual Studio est une idée plutôt douteuse.


Cependant, le temps ne s'arrête pas et les étoiles dans le ciel ne sont pas pressées de changer. Mais à ce moment-là, Jetbrains Rider était devenu un outil complet et pratique, et .NET Core pour Linux n'y fait pas mal en un coup d'œil.


La question était - quel langage fonctionnel choisir. Le fait qu'il devrait s'agir simplement d'un langage fonctionnel - sous une forme quelque peu pathétique, je l'ai expliqué ci-dessus.
Haskell, Idris, Agda ? F# - Je ne le connais pas. Une belle occasion d'apprendre de nouvelles couleurs du monde des langages fonctionnels.


Oui, F# pas purement fonctionnel. Mais qu'est-ce qui empêche d'adhérer à la " pureté "? Et puis il s'est avéré - que la documentation F # est assez détaillée et complète. Lisible, et je dirais même intéressant.


Qu'est-ce que F# pour moi maintenant? Un langage assez flexible, avec des IDE très pratiques (Rider, Visual Studio). Types complètement développés (bien que bien sûr Idris très loin). Et dans l'ensemble assez doux en termes de lisibilité. Cependant, il s'est avéré que sa « non-pureté » fonctionnelle - peut conduire le code à une forme complètement folle, à la fois en termes de lisibilité et de logique. L'analyse des paquets dans Nuget le démontre.


Une autre caractéristique intéressante et mystérieuse pour moi a été la découverte que personne n'était intéressé à écrire la formalisation RISC-V ISA en F # auparavant (officiellement ou sous une forme consultable). Et cela signifie que j'ai la chance d'introduire un nouveau flux dans cette communauté, cette langue et cet « écosystème ».


Les pièges que j'ai rencontrés


La partie la plus difficile a été la mise en œuvre du flux d'exécution. Il s'est souvent avéré que le fonctionnement de l'instruction n'était pas tout à fait clair. Malheureusement, je ne pouvais pas demander à un camarade fiable qui pouvait appeler à 3 heures du matin avec une voix inquiète et aspirée: "Vous savez, l'instruction BLTU est probablement différente en signextend ..." En ce sens, avoir des camarades qualifiés qui vous aideront avec un mot aimable et des conseils qualifiés appropriés est le bienvenu.


Quelles ont été les difficultés et les pièges. Je vais essayer la thèse:


  • ELF - une tâche curieuse était de comprendre comment travailler avec lui, lire des sections, des instructions. Très probablement, cette histoire dans le cadre du projet actuel n'est pas terminée.
  • des instructions non signées conduisaient périodiquement à des erreurs que j'ai détectées lors des tests unitaires
  • l'implémentation du travail avec la mémoire nécessaire pour penser à de beaux algorithmes de composition d'octets lisibles
  • il n'y avait pas de package approprié pour travailler avec des bits sous int32, int64 . Il a fallu du temps pour écrire mon package et le tester.
    Ici, je veux noter que travailler avec des bits en F # est beaucoup plus pratique que dans Haskell avec ses Data.Bits
  • prise en charge appropriée des bits de registre, avec la possibilité de prendre en charge x32 et x64 en même temps. L'inattention m'a amené à utiliser l' int64 à certains endroits. Les tests unitaires m'ont aidé à identifier cela. Mais cela a pris du temps.
  • Je n'ai pas trouvé de package CLI F # simple, concis et personnellement pratique pour moi personnellement. Un effet secondaire était d'écrire une version minimaliste dans un style fonctionnel.
  • Pour le moment, la mise en œuvre correcte des instructions système reste un mystère: FENCE, ECALL, BREAK
  • loin de l'ensemble des extensions (extensions ISA) de la liste: [A, M, C, F, D] actuellement évidentes. En particulier, l'implémentation de [F,D] ne se [F,D] pas via soft float .
  • pour le moment, il n'y a pas de compréhension claire des instructions privilégiées, du module utilisateur, du travail avec les périphériques - hélas. Et c'est la voie de la recherche, des essais et des erreurs.
  • Il n'y a pas de ceinture noire pour écrire des programmes d'assembleur sous RISC-V. Ce sera peut-être loin d'être souvent un besoin, étant donné le nombre de langues déjà portées pour l'écriture sous RISC-V.
  • le facteur temps était également important - il est assez faible dans le maelström du travail de base, des besoins quotidiens et de l'océan de la vie autour. Et il y a beaucoup de travail, et la plus grande partie n'est pas tant dans le « codage » - l'écriture du code lui-même, mais dans l'apprentissage, la maîtrise des matériaux.

Comment ça marche et quelles fonctionnalités


Maintenant peut-être la partie la plus technique . Quelles sont les fonctionnalités en ce moment:


  • rv32i jeu d'instructions rv32i
  • la possibilité d'exécuter le programme en tant que simulateur RISC-V - l'exécution de fichiers ELF.
  • prise en charge de la ligne de commande (CLI) - sélection de l'architecture exécutable, ensemble d'instructions, fichiers ELF exécutables, mode de journalisation, aide en ligne de commande.
  • la possibilité d'afficher le journal des instructions exécutables, proche de la vue objdump lors du démontage.
  • la possibilité d'exécuter des tests couvrant l'ensemble des instructions implémentées.

Le programme est divisé en plusieurs étapes et cycles:


  • lire la ligne de commande
  • lecture des instructions d'un fichier ELF
  • lecture d'une instruction spécifique en fonction du compteur actuel du PC (Program Counter)
  • instructions de décodage
  • exécution d'instructions
  • en cas de situations imprévues, des pièges sont mis en place, vous permettant de terminer le processus d'exécution, de signaler un problème et de fournir les données nécessaires
  • si le programme n'est pas dans une boucle infinie - afficher l'état des registres et terminer le programme de simulation

Ce qui est inclus dans les plans:


  • Base standard 64i (presque complète)
  • Extension standard M (multiplication / division entière)
  • Extension standard A (opérations de mémoire atomique)
  • Extension standard C (instructions 16 bits compressées)
  • Extension standard F (virgule flottante simple précision)
  • Extension standard D (virgule flottante double précision * niveau de privilège M (machine)
  • Niveau de privilège U (utilisateur)
  • Niveau de privilège S (superviseur)
  • Schémas de mémoire virtuelle SV32, SV39 et SV48
  • programmes d'accueil
  • GPIO - travailler avec des périphériques

Comment courir


Pour exécuter le programme, vous devez disposer de .NET Core . Si vous ne l'avez pas installé, alors, par exemple, sous Ubuntu 16.04 vous devez exécuter l'ensemble de commandes suivant:


 $ wget -q https://packages.microsoft.com/config/ubuntu/16.04/packages-microsoft-prod.deb -O packages-microsoft-prod.deb $ sudo dpkg -i packages-microsoft-prod.deb $ sudo apt-get update $ sudo apt-get install apt-transport-https $ sudo apt-get update $ sudo apt-get install dotnet-sdk-3.0 

Pour vérifier que quelque chose dans la vie a changé, exécutez:


 $ dotnet --version 

Et la vie devrait briller de nouvelles couleurs!


Essayez maintenant de courir. Pour ce faire, stockez votre thé ou café préféré, du chocolat avec des petits pains, allumez votre musique préférée et suivez cet ensemble de commandes:


 $ cd some/my/dev/dir $ git clone https://github.com/mrLSD/riscv-fs $ cd riscv-fs $ dotnet build $ dotnet run -- --help 

et votre console devrait vous faire un clin d'œil ludique avec un message d'aide.
Le lancement est:


 $ dotnet run 

D'un ton strict, il dira que des paramètres sont nécessaires. Par conséquent, exécutez:


 $ dotnet run -- -A rv32i -v myapp.elf 

C'est le même moment gênant quand il s'avère que nous avons encore besoin d'un programme prêt à l' emploi prêt à exécuter pour RISC-V. Et il y a quelque chose pour moi pour vous aider. Cependant, vous aurez besoin de la chaîne d'outils GNU pour RISC-V . Qu'il soit installé comme devoir - la description du référentiel décrit suffisamment en détail comment procéder.


Ensuite, pour obtenir le fichier ELF de test convoité, nous effectuons les actions suivantes:


 $ cd Tests/asm/ $ make build32 

si vous avez une chaîne d'outils RISC-V, alors tout devrait bien se passer. Et les fichiers devraient s'afficher dans le répertoire:


 $ ls Tests/asm/build/ add32 alu32 alui32 br32 j32 mem32 sys32 ui32 

et maintenant hardiment, sans regarder en arrière, nous essayons la commande:


 $ dotnet run -- -A rv32i -v Tests/asm/build/ui32 

Il est important de noter que Tests/asm pas un programme de test, mais leur objectif principal est les instructions de test et leurs codes pour écrire des tests. Par conséquent, si vous aimez quelque chose de plus grand et de plus héroïque, changer le monde dans votre volonté consiste à trouver un fichier ELF 32 bits exécutable indépendamment qui ne prend en charge que les instructions rv32i .


Cependant, l'ensemble d'instructions et d'extensions sera reconstitué, prendra de l'ampleur et prendra du poids.


Résumé et liens


Cela s'est avéré être une petite narration pathétique parfumée par l'histoire personnelle. Parfois technique, parfois subjectif. Cependant enthousiaste et avec une touche d'enthousiasme.


Pour ma part, je suis intéressé de vous entendre: critiques, impressions, bons mots d'adieu. Et pour les plus audacieux - aidez à soutenir le projet.


Êtes-vous intéressé par un tel format narratif et souhaitez-vous continuer?


Source: https://habr.com/ru/post/fr473714/


All Articles