Ce référentiel contient une spécification formelle de l'architecture RISC-V, écrite en voile. Il a été adopté par la Fondation RISC-V.
Le modèle spécifie les formats de langage d'assemblage des instructions, les encodeurs et décodeurs correspondants et la sémantique d'instructions. Un guide de lecture du modèle est fourni dans le DOC / sous-répertoire, ainsi qu'un guide sur la façon d'étendre le modèle.
Les définitions de latex ou d'Asciidoc peuvent être générées à partir du modèle qui convient à l'inclusion dans la documentation de référence. Il y a aussi la nouvelle prise en charge de la documentation Sail Asciidoctor pour RISC-V.
Sail est un langage pour décrire la sémantique des processeurs d'architecture d'instructions (ISA): la spécification architecturale du comportement des instructions de la machine. Sail est un langage adapté aux ingénieurs, un peu comme le pseudocode du fournisseur antérieur, mais plus précisément défini et avec des outils pour prendre en charge une large gamme de cas d'utilisation.
Compte tenu d'une spécification de voile, l'outil peut le taper à le vérifier, générer des extraits de documentation (en latex ou ASCIIDOC), générer des émulateurs exécutables, afficher la couverture des spécifications, générer des versions de l'ISA pour les outils de modèle de mémoire détendus, prendre en charge la génération de test de séquence d'instructions automatisées, Générer les définitions de théorème-prover pour la preuve interactive (dans Isabelle, Hol4 et CoQ), la preuve de prise en charge du code binaire (dans Islaris) et (en cours) générer un modèle ISA de référence dans Systemverilog qui peut être utilisé pour la vérification du matériel formel.
La voile est utilisée pour plusieurs descriptions ISA, y compris les versions essentiellement complètes du comportement séquentiel d'ARM-A (dérivé automatiquement de la spécification autoritaire ARM-Interne RISC-V, Cheriot, MIPS et Cheri-mips; Tout cela est suffisamment complet pour démarrer divers systèmes d'exploitation. Il existe également des modèles SAIL pour les plus petits fragments d'IBM Power et X86, y compris une version du modèle ACL2 X86 traduit automatiquement à partir de cela.
Installez la voile. Sur Linux, vous pouvez télécharger une version binaire (fortement recommandée), ou vous pouvez installer à partir de Source à l'aide d'Opam. Alors:
$ make
Construirea le simulateur dans c_emulator/riscv_sim_RV64 .
Si vous recevez un message d'erreur disant sail: unknown option '--require-version'. C'est parce que votre compilateur de voile est trop vieux. Vous avez besoin de version 0.18 ou ultérieure.
On peut construire le modèle RV32 ou RV64 en spécifiant ARCH=RV32 ou ARCH=RV64 sur la ligne make , et en utilisant le suffixe cible correspondant. RV64 est construit par défaut, mais le modèle RV32 peut être construit en utilisant:
$ ARCH=RV32 make
qui crée le simulateur dans c_emulator/riscv_sim_RV32 .
Le makefile cible riscv_isa_build , riscv_coq_build et riscv_hol_build invoque le prover respectif pour traiter les définitions et produire le modèle Isabelle dans generated_definitions/isabelle/RV64/Riscv.thy , le modèle Coq dans le generated_definitions/coq/RV64/riscv.v Modèle dans generated_definitions/hol4/RV64/riscvScript.sml respectivement. Nous avons testé Isabelle 2018, CoQ 8.8.1 et Hol4 Kananaskis-12. Lors de la construction de ces cibles, veuillez vous assurer que les bibliothèques de prover correspondantes dans le répertoire SAIL ( $SAIL_DIR/lib/$prover ) sont à jour et construites, par exemple en make dans ces répertoires.
Le simulateur peut être utilisé pour exécuter de petits binaires de test.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
Une suite de programmes de test RV32 et RV64 dérivées de la suite riscv-tests est incluse sous Test / RISCV-Tests /. La suite de test peut être exécutée à l'aide test/run_tests.sh .
Des informations sur les options de configuration pour le simulateur sont disponibles sur ./c_emulator/riscv_sim_<arch> -h .
Certaines options utiles sont les suivantes: configurer si les accès mal alignés TRAP ( --enable-misaligned ), et si les promenades de page de page mettent à jour les bits PTE ( --enable-dirty-update ).
Pour démarrer les images du système d'exploitation, consultez les informations sous le OS-boot / sous-répertoire.
Rarement, la version de version de Sail peut ne pas répondre à vos besoins. Cela pourrait se produire si vous avez besoin d'un correctif de bogue ou d'une nouvelle fonctionnalité non encore dans la version Sail publiée, ou si vous travaillez activement sur Sail. Dans ce cas, vous pouvez dire au sail-riscv Makefile d'utiliser une copie locale de Sail en fixant SAIL_DIR à la racine d'une caisse du repo de voile lorsque vous make . Alternativement, vous pouvez utiliser opam pin pour installer la voile à partir d'un caisse locale du dépôt de voile comme décrit dans les instructions d'installation de voile.
Ce sont des extraits textuels du fichier modèle contenant les instructions de base, RISCV_INSTS_BASE.SAIL, avec quelques commentaires ajoutés.
/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */
union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
/* the encode/decode mapping between AST elements and 32-bit words */
mapping encdec_iop : iop <-> bits(3) = {
RISCV_ADDI <-> 0b000,
RISCV_SLTI <-> 0b010,
RISCV_SLTIU <-> 0b011,
RISCV_ANDI <-> 0b111,
RISCV_ORI <-> 0b110,
RISCV_XORI <-> 0b100
}
mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
/* the execution semantics for the ITYPE instructions */
function clause execute (ITYPE (imm, rs1, rd, op)) = {
let rs1_val = X(rs1);
let immext : xlenbits = sign_extend(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
};
X(rd) = result;
RETIRE_SUCCESS
}
/* the assembly/disassembly mapping between AST elements and strings */
mapping itype_mnemonic : iop <-> string = {
RISCV_ADDI <-> "addi",
RISCV_SLTI <-> "slti",
RISCV_SLTIU <-> "sltiu",
RISCV_XORI <-> "xori",
RISCV_ORI <-> "ori",
RISCV_ANDI <-> "andi"
}
mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
union clause ast = SRET : unit
mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute SRET() = {
let sret_illegal : bool = match cur_privilege {
User => true,
Supervisor => not(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
Machine => not(extensionEnabled(Ext_S))
};
if sret_illegal
then { handle_illegal(); RETIRE_FAIL }
else if not(ext_check_xret_priv (Supervisor))
then { ext_fail_xret_priv(); RETIRE_FAIL }
else {
set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_SUCCESS
}
}
mapping clause assembly = SRET() <-> "sret"
Le modèle construit un émulateur C qui peut exécuter des fichiers ELF RISC-V, et les deux émulateurs fournissent une prise en charge de la plate-forme suffisante pour démarrer Linux, FreeBSD et Sel4. L'émulateur C peut être lié à l'émulateur de pointe pour exécution avec une vérification tandem par instruction.
L'émulateur C, pour le Boot Linux, fonctionne actuellement à environ 300 KIPS sur un Intel i7-7700 (lorsque le traçage détaillé par instruction est désactivé), et il existe de nombreuses opportunités d'optimisation future (le modèle Sail MIPS fonctionne à environ 1 MIPS ). Cela permet de démarrer Linux en environ 4 minutes et FreeBSD en environ 2 minutes. L'utilisation de la mémoire pour l'émulateur C lors du démarrage de Linux est d'environ 140 Mo.
Les fichiers du répertoire de l'émulateur C implémentent le chargement ELF et les périphériques de plate-forme, définit la carte de mémoire physique et utilisent des options de ligne de commande pour sélectionner des choix ISA spécifiques à l'implémentation.
L'émulateur C généré par la voile peut mesurer la couverture des succursales de spécification de tous les tests exécutés, affichant les résultats sous forme de tables par fichier et en tant que versions annotées par HTML de la source du modèle.
Pour la vérification en tandem des flux d'instructions aléatoires, les outils prennent en charge les protocoles utilisés dans TestRig pour injecter directement des instructions dans l'émulateur C et produire des informations traces au format RVFI. Cela a été utilisé pour les tests croisés contre Spike et la spécification RVBS écrite dans Bluespec Systemverilog.
L'émulateur C peut également être directement lié à Spike, qui fournit une vérification en tandem sur les binaires ELF (y compris les bottes de système d'exploitation). Ceci est souvent utile pour déboguer les problèmes de démarrage du système d'exploitation dans le modèle lorsque le démarrage est connu en travaillant sur Spike. Il est également utile de détecter les choix d'implémentation spécifiques à la plate-forme dans Spike qui ne sont pas mandatés par la spécification ISA.
Le modèle ISA est intégré au modèle opérationnel du modèle de mémoire détendue RISC-V, RVWMO (comme décrit dans une annexe de la spécification au niveau de l'utilisateur RISC-V), qui est l'un des modèles de référence utilisés dans le développement du RISC -V architecture de concurrence; Cela fait partie de l'outil RMEM. Il est également intégré au modèle de concurrence axiomatique RISC-V dans le cadre de l'outil ISLA-axiomatique.
Dans le cadre des travaux d'architecture de concurrence de l'Université de Cambridge / INRIA, ces groupes ont produit et publié une bibliothèque d'environ 7 000 tests de découverte. Les modèles de concurrence RISC-V opérationnels et axiomatiques sont synchronisés pour ces tests, et ils sont en outre d'accord avec le comportement architecté du bras correspondant pour les tests en commun.
Ces tests ont également été effectués sur le matériel RISC-V, sur un conseil d'administration Multicore Proto SIFIVE RISC-V FU540 (Freedom Unleashed), aimablement prêté par Imperas. À ce jour, un comportement séquentiellement cohérent a été observé là-bas.
Sail vise à soutenir la génération de définitions de prover du théorème idiomatique sur plusieurs outils. À l'heure actuelle, il prend en charge Isabelle, Hol4 et CoQ, et le répertoire prover_snapshots fournit des instantanés des définitions de proverage du théorème généré.
Ces traductions de théorème-prover peuvent cibler plusieurs monades à différentes fins. Le premier est une monade d'État avec un non-déterminisme et des exceptions, adapté au raisonnement dans un cadre séquentiel, en supposant que les expressions effectives sont exécutées sans interruptions et avec un accès exclusif à l'État.
Pour le raisonnement sur la concurrence, où les instructions s'exécutent hors de commande, de manière spéculative et non atomiquement, il y a une monade libre sur un type de données d'effet des actions de mémoire. Cette monade est également utilisée dans le cadre du support de concurrence susmentionné via l'outil RMEM.
Les fichiers sous handwritten_support fournissent des définitions de bibliothèque pour CoQ, Isabelle et Hol4.
sail-riscv
- model // Sail specification modules
- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories
- c
- lem
- isabelle
- coq
- hol4
- latex
- prover_snapshots // snapshots of generated theorem prover definitions
- handwritten_support // prover support files
- c_emulator // supporting platform files for C emulator
- doc // documentation, including a reading guide
- test // test files
- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
- os-boot // information and sample files for booting OS images
Le modèle est mis à disposition en vertu de la licence BSD en deux clauses en licence.
Écrit à l'origine par Prashanth Mundkur à SRI International, et développé par d'autres, en particulier les chercheurs de l'Université de Cambridge.
Voir LICENCE et le blâme GIT pour une liste complète des auteurs.
Ce logiciel a été développé par ce qui précède dans le projet rigoureux d'ingénierie des systèmes grand public (REMS), en partie financé par l'EPSRC Grant EP / K008528 / 1, dans les universités de Cambridge et d'Edimbourg.
Ce logiciel a été développé par SRI International et le University of Cambridge Computer Laboratory (Department of Computer Science and Technology) sous le contrat DARPA / AFRL FA8650-18-C-7809 ("CIFV"), et dans le cadre du contrat DARPA HR0011-18-C- 0016 ("ECATS") dans le cadre du programme de recherche Darpa Ssith.
Ce projet a reçu un financement du Conseil européen de recherche (ERC) dans le cadre du programme de recherche et d'innovation Horizon 2020 de l'Union européenne (accord de subvention 789108, Elver).
