Este repositorio contiene una especificación formal de la arquitectura RISC-V, escrita en vela. Ha sido adoptado por la Fundación RISC-V.
El modelo especifica los formatos de lenguaje de ensamblaje de las instrucciones, los codificadores y decodificadores correspondientes, y la semántica de instrucciones. Se proporciona una guía de lectura para el modelo en el DOC/ subdirectorio, junto con una guía sobre cómo extender el modelo.
Las definiciones de látex o asciidoc se pueden generar a partir del modelo que son adecuados para su inclusión en la documentación de referencia. También existe el nuevo soporte de documentación de ASCIIDOCTOR SAIL para RISC-V.
Sail es un lenguaje para describir la semántica de la arquitectura del conjunto de instrucciones (ISA) de los procesadores: la especificación arquitectónica del comportamiento de las instrucciones de la máquina. Sail es un lenguaje amigable para el ingeniero, al igual que el pseudocódigo del proveedor anterior, pero con más precisión definida y con herramientas para admitir una amplia gama de casos de uso.
Dada una especificación de navegación, la herramienta puede verificarla, generar fragmentos de documentación (en látex o asciidoc), generar emuladores ejecutables, mostrar cobertura de especificaciones, generar versiones de la ISA para herramientas de modelos de memoria relajada, admitir la generación de pruebas de secuencia de instrucciones automatizadas, Genere las definiciones de Proverso del Teorema para la prueba interactiva (en Isabelle, HOL4 y COQ), admite pruebas sobre el código binario (en islaris) y (en progreso) generan un modelo ISA de referencia en Systemverilog que puede usarse para la verificación formal de hardware.
Se está utilizando SAIL para múltiples descripciones ISA, incluidas versiones esencialmente completas del comportamiento secuencial de ARM-A (derivado automáticamente de la especificación de brazo autorizado, y liberado bajo una licencia BSD clara con permiso de ARM), Risc-V, Cheri- Risc-V, Cheriot, MIPS y Cheri-Mips; Todos estos son lo suficientemente completos como para arrancar varios sistemas operativos. También hay modelos de vela para fragmentos más pequeños de IBM Power y X86, incluida una versión del modelo ACL2 X86 traducido automáticamente de eso.
Instale la vela. En Linux puede descargar una versión binaria (muy recomendable), o puede instalar desde la fuente con OPAM. Entonces:
$ make
construirá el simulador en c_emulator/riscv_sim_RV64 .
Si recibe un mensaje de error que dice sail: unknown option '--require-version'. Es porque tu compilador de vela es demasiado viejo. Necesita la versión 0.18 o posterior.
Uno puede construir el modelo RV32 o RV64 especificando ARCH=RV32 o ARCH=RV64 en la línea make , y utilizando el sufijo objetivo coincidente. RV64 se construye de forma predeterminada, pero el modelo RV32 se puede construir usando:
$ ARCH=RV32 make
que crea el simulador en c_emulator/riscv_sim_RV32 .
El Makefile se dirige riscv_isa_build , riscv_coq_build y riscv_hol_build Invok the Respective Prover para procesar las definiciones y producir el modelo Isabelle en generated_definitions/isabelle/RV64/Riscv.thy , el modelo coq en generated_definitions/coq/RV64/riscv.v . o el modelo coq en generado modelo en generated_definitions/hol4/RV64/riscvScript.sml respectivamente. Hemos probado Isabelle 2018, Coq 8.8.1 y Hol4 Kananaskis-12. Al construir estos objetivos, asegúrese de que las bibliotecas de Prover correspondientes en el directorio de Sail ( $SAIL_DIR/lib/$prover ) estén actualizados y construidos, por ejemplo, ejecutando make en esos directorios.
El simulador se puede usar para ejecutar pequeños binarios de prueba.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
Un conjunto de programas de prueba RV32 y RV64 derivados de la suite de prueba riscv-tests se incluye en Test/RISCV-Tests/. La suite de prueba se puede ejecutar usando test/run_tests.sh .
La información sobre las opciones de configuración para el simulador ./c_emulator/riscv_sim_<arch> -h disponible.
Algunas opciones útiles son: configurar si los accesos desalineados trampa ( --enable-misaligned ), y si la tabla de página actualiza los bits de PTE ( --enable-dirty-update ).
Para iniciar imágenes del sistema operativo, consulte la información debajo del OS-Boot/ Subdirectory.
Raramente, la versión de lanzamiento de Sail puede no satisfacer sus necesidades. Esto podría suceder si necesita una corrección de errores o una nueva función aún no en la versión de vela lanzada, o está trabajando activamente en Sail. En este caso, puede decirle a la Makefile sail-riscv que use una copia local de Sail al establecer SAIL_DIR a la raíz de un pago del repositorio de la vela cuando make . Alternativamente, puede usar opam pin para instalar Sail desde un pago local del repositorio de la vela como se describe en las instrucciones de instalación de Sail.
Estos son extractos literales del archivo del modelo que contiene las instrucciones base, riscv_insts_base.sail, con algunos comentarios agregados.
/* 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"
El modelo construye un emulador C que puede ejecutar archivos ELF RISC-V, y ambos emuladores proporcionan soporte de plataforma suficiente para arrancar Linux, FreeBSD y SEL4. El emulador C se puede vincular contra el emulador de espiga para su ejecución con verificación en tándem por instrucción.
El emulador C, para el arranque de Linux, actualmente se ejecuta a aproximadamente 300 kips en un Intel i7-7700 (cuando el rastreo detallado por instrucción está deshabilitado), y hay muchas oportunidades para la optimización futura (el modelo Sail MIPS se ejecuta en aproximadamente 1 MIPS ). Esto permite que uno inicie Linux en aproximadamente 4 minutos, y FreeBSD en aproximadamente 2 minutos. El uso de la memoria para el emulador C al arrancar Linux es de aproximadamente 140 MB.
Los archivos en el directorio del emulador C implementan la carga ELF y los dispositivos de la plataforma, definen el mapa de memoria física y usan opciones de línea de comandos para seleccionar opciones ISA específicas de implementación.
El emulador C generado por la vela puede medir la cobertura de la rama de especificación de cualquier prueba ejecutada, mostrando los resultados como tablas por archivo y como versiones anotadas por HTML de la fuente del modelo.
Para la verificación en tándem de flujos de instrucciones aleatorios, las herramientas admiten los protocolos utilizados en TestRig para inyectar directamente instrucciones en el emulador C y producir información de trazas en formato RVFI. Esto se ha utilizado para pruebas cruzadas contra SPIKE y la especificación RVBS escrita en Bluespec SystemVerilog.
El emulador C también se puede vincular directamente a Spike, que proporciona verificación en tándem en binarios de elfos (incluidas las botas del sistema operativo). Esto a menudo es útil para depurar problemas de arranque del sistema operativo en el modelo cuando se conoce el arranque trabajando en Spike. También es útil detectar opciones de implementación específicas de la plataforma en pico que no son obligatorias por la especificación ISA.
El modelo ISA está integrado con el modelo operativo del modelo de memoria relajada RISC-V, RVWMO (como se describe en un apéndice de la especificación de nivel de usuario RISC-V), que es uno de los modelos de referencia utilizados en el desarrollo del RISC -V arquitectura de concurrencia; Esto es parte de la herramienta RMEM. También está integrado con el modelo de concurrencia axiomática RISC-V como parte de la herramienta isla-axiomática.
Como parte del trabajo de arquitectura de concurrencia de la Universidad de Cambridge/ Inria, esos grupos produjeron y lanzaron una biblioteca de aproximadamente 7000 pruebas de fuego. Los modelos de concurrencia RISC-V operacionales y axiomáticos están sincronizados para estas pruebas, y además están de acuerdo con el comportamiento diseñado por el brazo correspondiente para las pruebas en común.
Esas pruebas también se han ejecutado en hardware RISC-V, en un tablero de Proto Multicore de Sifive RISC-V FU540 (Freedom Unleashed), amablemente prestado de Imperas. Hasta la fecha, solo se observó un comportamiento secuencialmente consistente.
Sail tiene como objetivo apoyar la generación de definiciones de prover del teorema idiomático en múltiples herramientas. En la actualidad, es compatible con Isabelle, Hol4 y Coq, y el directorio prover_snapshots proporciona instantáneas de las definiciones de prover del teorema generado.
Estas traducciones de retroceso del teorema pueden dirigirse a múltiples mónadas para diferentes fines. El primero es una mónada estatal con no determinismo y excepciones, adecuado para el razonamiento en un entorno secuencial, suponiendo que las expresiones efectivas se ejecutan sin interrupciones y con acceso exclusivo al estado.
Para razonar sobre la concurrencia, donde las instrucciones se ejecutan fuera de pedido, especulativamente y no atómicamente, hay una mónada libre sobre un tipo de datos de efecto de las acciones de memoria. Esta mónada también se usa como parte del soporte de concurrencia antes mencionado a través de la herramienta RMEM.
Los archivos bajo handwritten_support proporcionan definiciones de biblioteca para Coq, Isabelle y 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
El modelo está disponible bajo la licencia BSD de dos cláusulas en la licencia.
Originalmente escrito por Prashanth Mundkur en SRI International, y desarrollado por otros, especialmente investigadores de la Universidad de Cambridge.
Consulte LICENCE y la culpa de Git por una lista completa de autores.
Este software fue desarrollado por lo anterior dentro de la rigurosa ingeniería del proyecto de sistemas convencionales (REMS), financiado en parte por EPSRC Grant EP/K008528/1, en las universidades de Cambridge y Edimburgo.
Este software fue desarrollado por SRI International y el Laboratorio de Computación de Computación de la Universidad de Cambridge (Departamento de Ciencias y Tecnología de la Comportación) bajo el contrato DARPA/AFRL FA8650-18-C-7809 ("CIFV"), y bajo el contrato DARPA HR0011-18-C- 0016 ("ECATS") como parte del programa de investigación DARPA SSTH.
Este proyecto ha recibido fondos del Consejo Europeo de Investigación (ERC) bajo el Programa de Investigación e Innovación del Horizon 2020 de la Unión Europea (Acuerdo de subvención 789108, Elver).
