📋 🛂 👐🏾 Cómo llegué a la especificación formal de un procesador RISC-V en F # 🗾 👆 👊🏾

En las lánguidas noches de invierno, cuando el sol pasaba perezosamente a través del velo de los días, encontraba la fuerza para enfrentar la realización de un sueño de larga data: descubrir cómo están dispuestos los procesadores. Este sueño me llevó a escribir una especificación formal del procesador RISC-V. Proyecto Github

imagen

Como fue

Tenía ese deseo hace mucho tiempo, cuando hace 20 años comencé a participar en mis primeros proyectos. En su mayor parte, se trataba de investigación científica, modelado matemático en el marco de trabajos y artículos científicos. Estos fueron los días de Pascal y Delfos. Sin embargo, incluso entonces, Haskell y la programación funcional atrajeron mi interés. Pasó el tiempo, cambiaron los idiomas de los proyectos y las tecnologías en las que estuve involucrado. Pero desde entonces, el interés en los lenguajes de programación funcionales ha sido un hilo común, y se han convertido en: Haskell, Idris, Agda. Recientemente, sin embargo, mis proyectos han estado en Rust. Una inmersión más profunda en Rust me llevó a estudiar dispositivos integrados.

De óxido a incrustado

Las capacidades de Rust son tan amplias y la comunidad es tan activa que el desarrollo integrado ha comenzado a admitir una amplia gama de dispositivos. Y este fue mi primer paso hacia una comprensión más baja de los procesadores.

Mi primer tablero fue: STM32F407VET6 . Fue una inmersión en el mundo de los microcontroladores, de los cuales en ese momento estaba muy lejos, y entendí aproximadamente lo suficiente como se hacía el trabajo en un nivel bajo.

Poco a poco, esp32 , ATmega328 juntas (representadas por la junta de Ucrania UNO ) se agregaron aquí. La inmersión en stm32 resultó ser bastante dolorosa: la información es abundante y, a menudo, no es la que necesito. Y resultó que desarrollar, por ejemplo, en Assembler es una tarea bastante rutinaria e ingrata, con su subconjunto de más de 1000 instrucciones. Sin embargo, Rust enfrentó esto alegremente, aunque a veces hubo dificultades con la integración de juntas chinas específicas.

La arquitectura AVR resultó ser notablemente más simple y más transparente. Los abundantes manuales me dieron una comprensión suficiente de cómo trabajar con un conjunto de instrucciones tan limitado y, sin embargo, ser capaz de crear soluciones muy interesantes. Sin embargo, el camino de Arduino no me complació en absoluto, pero escribir en Asm / C / Rust resultó ser mucho más interesante.

¿Dónde está el RISC-V?

Y en ese momento surge una pregunta lógica: ¿dónde está la CPU RISC-V ?
Debido a la naturaleza minimalista de AVR y su documentación suficiente, volví a mi sueño anterior para descubrir cómo funciona el procesador. En este momento, tenía una placa FPGA y las primeras implementaciones para ella en forma de interacción con dispositivos VGA, salida de gráficos, interacción con periféricos.

Los libros fueron mis guías para la arquitectura del procesador:

John L. Hennessy y David A. Patterson - Arquitectura de computadoras: un enfoque cuantitativo (Serie Morgan Kaufmann en Arquitectura y diseño de computadoras)
John L. Hennessy y David A. Patterson - Organización y diseño de computadoras. La interfaz hardware / software: Edición RISC-V
David M. Harris y Sarah L. Harris - Circuitos digitales y arquitectura de computadoras
El manual del conjunto de instrucciones RISC-V

Porque es necesario

Parece que todo ya se ha escrito e implementado durante mucho tiempo.

diversas implementaciones en HDL y lenguajes de programación. Por cierto, una implementación bastante interesante de RISC-V en Rust .

Sin embargo, qué podría ser más interesante que descubrirlo usted mismo y crear el suyo propio. Tu bici ¿O contribuir a la construcción de bicicletas ? Además del profundo interés personal, tuve una idea: cómo tratar de popularizar, interesar. Y encuentre su forma, su enfoque. Y eso significa presentar la documentación RISC-V ISA bastante aburrida en forma de una especificación oficial en una forma diferente. Y me parece que el camino de la formalización en este sentido es bastante interesante.

¿Qué quiero decir con formalización? Un concepto bastante amplio. Representación de un conjunto de datos específico en forma formal. En este caso, a través de una descripción de estructuras y una descripción funcional. Y en este sentido, los lenguajes de programación funcionales tienen su propio encanto. Además, la tarea es que una persona que no esté muy inmersa en la programación pueda leer el código como una especificación, si es posible, comprender mínimamente los detalles del lenguaje en el que se describe.
Un enfoque declarativo, por así decirlo. Hay una declaración, pero cómo funciona exactamente ya no es esencial. Lo principal es la legibilidad, la visibilidad y, por supuesto, la corrección. Correspondencia de las declaraciones formales con el significado incrustado en ellas.
imagen
Total: tengo mucha curiosidad por transmitir mi interés a los demás. Existe una cierta ilusión de que el interés es la fuerza impulsora de las acciones. A través del cual la individualidad se vuelve y se manifiesta Y esto es parte de la autorrealización, la encarnación de la creatividad.
Ambicioso y un poco de letra. Que sigue

Implementaciones existentes

Existen y actualmente están siendo agregados por el proyecto: Verificación formal RISC-V .
Lista de especificaciones formales (incluido mi trabajo): https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/references.md

Como puede ver, en su mayor parte se trata de formalizaciones en el idioma Haskell. Este fue el punto de partida para elegir un lenguaje funcional diferente. Y mi elección recayó en F # .

¿Por qué `F#`

Dio la casualidad de que he sabido sobre F # durante mucho tiempo, pero de alguna manera en el ajetreo de la vida cotidiana no tuve la oportunidad de conocernos mejor. Otro factor fue la plataforma .NET . Teniendo en cuenta que estoy bajo Linux, durante mucho tiempo no estaba contento con el IDE, y mono parecía lo suficientemente crudo. Y regresar a Windows solo por MS Visual Studio es una idea bastante dudosa.

Sin embargo, el tiempo no se detiene, y las estrellas en el cielo no tienen prisa por cambiar. Pero en este momento, Jetbrains Rider se había convertido en una herramienta completa y conveniente, y .NET Core para Linux no trae dolor de un vistazo.

La pregunta era: qué lenguaje funcional elegir. El hecho de que debería ser solo un lenguaje funcional, en una forma algo patética, discutí anteriormente.
Haskell, Idris, Agda ? F# - No estoy familiarizado con él. Una gran ocasión para aprender nuevos colores del mundo de los lenguajes funcionales.

Sí, F# no F# puramente funcional. Pero, ¿qué impide adherirse a la " pureza "? Y luego resultó que la documentación de F # es bastante detallada y completa. Legible, e incluso diría interesante.

¿Qué es F# para mí ahora? Un lenguaje bastante flexible, con IDEs muy convenientes (Rider, Visual Studio). Tipos completamente desarrollados (aunque, por supuesto, Idris muy lejos). Y en general bastante dulce en términos de legibilidad. Sin embargo, como resultó, su " no limpieza " funcional puede llevar el código a una forma completamente loca, tanto en términos de legibilidad como de lógica. El análisis de paquetes en Nuget demuestra esto.

Otra característica interesante y misteriosa para mí fue el descubrimiento de que nadie estaba interesado en escribir la formalización RISC-V ISA en F # antes (oficialmente o en forma de búsqueda). Y esto significa que tengo la oportunidad de introducir una nueva transmisión en esta comunidad, idioma y " ecosistema ".

Los escollos que encontré

La parte más difícil fue la implementación del flujo de ejecución. A menudo resultó que no estaba del todo claro cómo debería funcionar la instrucción. Desafortunadamente, un amigo confiable que podría ser llamado a las 3 en punto de la mañana y preguntado con una voz excitada y aspirada: "Sabes, la instrucción BLTU probablemente no se extienda de manera diferente ..." - No lo sé. En este sentido, tener compañeros calificados que ayuden con una palabra amable y un asesoramiento calificado apropiado es muy bienvenido.

Cuáles fueron las dificultades y dificultades. Probaré la tesis:

ELF: una tarea curiosa era descubrir cómo trabajar con él, leer secciones e instrucciones. Lo más probable es que esta historia en el marco del proyecto actual no esté terminada.
instrucciones sin firmar periódicamente condujeron a errores que detecté durante las pruebas unitarias
La implementación del trabajo con memoria requiere pensar en algoritmos de composición de bytes hermosos y legibles.
no había un paquete adecuado para trabajar con bits en int32, int64 . Me tomó tiempo escribir mi paquete y probarlo.
Aquí quiero señalar que trabajar con bits en F # es mucho más conveniente que en Haskell con sus datos.
soporte adecuado para bits de registro, con la capacidad de soportar x32 y x64 al mismo tiempo. La int64 de int64 me llevó a usar int64 en algunos lugares. Las pruebas unitarias me ayudaron a identificar esto. Pero tomó un tiempo.
No encontré un paquete CLI F # simple, conciso y personalmente conveniente para mí personalmente. Un efecto secundario fue escribir una versión minimalista en un estilo funcional.
Por el momento, sigue siendo un misterio cómo implementar correctamente las instrucciones del sistema: FENCE, ECALL, BREAK
lejos de todo el conjunto de extensiones (extensiones ISA) de la lista: [A, M, C, F, D] actualmente obvias. En particular, la implementación de [F,D] no se realiza mediante soft float .
Por el momento, no hay una comprensión clara de las instrucciones privilegiadas, Mod de usuario, trabajo con periféricos, por desgracia. Y esta es la forma de investigación, ensayo y error.
No hay cinturón negro para escribir programas Assembler bajo RISC-V. Quizás, lejos de ser frecuente, esto sea una necesidad, dada la cantidad de idiomas que ya se han portado para escribir bajo RISC-V.
el factor tiempo también fue significativo: es bastante pequeño en la vorágine del trabajo básico, las necesidades cotidianas y el océano de la vida. Y hay mucho trabajo, y la mayor parte no se trata tanto de " codificar " - escribir el código en sí, sino de aprender, dominar los materiales.

Cómo funciona y qué características tiene

Ahora quizás la parte más técnica . ¿Cuáles son las características en este momento?

rv32i conjunto de instrucciones rv32i
la capacidad de ejecutar el programa como un simulador RISC-V: la ejecución de archivos ELF.
soporte de línea de comando (CLI): selección de arquitectura ejecutable, conjunto de instrucciones, archivos ELF ejecutables, modo de registro, ayuda de línea de comando.
la capacidad de mostrar el registro de instrucciones ejecutables, cerca de la vista objdump al desmontar.
la capacidad de ejecutar pruebas que cubren todo el conjunto de instrucciones implementadas.

El programa se divide en tales etapas y ciclos:

leer la línea de comando
leer instrucciones de un archivo ELF
leer una instrucción específica de acuerdo con el contador actual de PC (Contador de programas)
instrucciones de decodificación
ejecución de instrucciones
En caso de situaciones imprevistas, se configuran trampas, lo que le permite completar el proceso de ejecución, señalar un problema y proporcionar los datos necesarios
Si el programa no está en un bucle infinito, muestre el estado de los registros y finalice el programa de simulación.

Lo que está incluido en los planes:

Base estándar 64i (casi completa)
Extensión estándar M (multiplicación / división de enteros)
Extensión estándar A (operaciones de memoria atómica)
Extensión estándar C (instrucciones comprimidas de 16 bits)
Extensión estándar F (coma flotante de precisión simple)
Extensión estándar D (coma flotante de precisión doble * Nivel de privilegio M (máquina)
Nivel de privilegio U (usuario)
Nivel de privilegio S (Supervisor)
Esquemas de memoria virtual SV32, SV39 y SV48
programas de acogida
GPIO - trabaja con periféricos

Como correr

Para ejecutar el programa, debe tener .NET Core . Si no lo tiene instalado, entonces, por ejemplo, en Ubuntu 16.04 debe ejecutar el siguiente conjunto de comandos:

 $ 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

Para verificar que algo en la vida ha cambiado, ejecute:

 $ dotnet --version

¡Y la vida debería brillar con nuevos colores!

Ahora intenta correr. Para hacer esto, almacene su té o café favorito, chocolate con bollos, encienda su música favorita y siga este conjunto de comandos:

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

y tu consola debería hacerte un guiño juguetón con un mensaje de ayuda.
El lanzamiento es:

 $ dotnet run

En un tono estricto, dirá que se necesitan parámetros. Por lo tanto, ejecute:

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

Este es el mismo momento incómodo cuando resulta que todavía necesitamos un programa listo para ejecutar para RISC-V. Y hay algo en lo que te puedo ayudar. Sin embargo, necesitará la cadena de herramientas GNU para RISC-V . Debe instalarse la tarea: la descripción del repositorio describe con suficiente detalle cómo hacer esto.

Luego, para obtener el codiciado archivo ELF de prueba, realizamos las siguientes acciones:

 $ cd Tests/asm/ $ make build32

Si tiene una cadena de herramientas RISC-V , todo debería funcionar sin problemas. Y los archivos deberían mostrarse en el directorio:

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

y ahora audazmente, sin mirar atrás, probamos el comando:

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

Es importante tener en cuenta que Tests/asm no Tests/asm un programa de prueba, pero su propósito principal son las instrucciones de prueba y sus códigos para escribir pruebas. Por lo tanto, si le gusta algo más grande y más heroico, entonces cambiar el mundo en su testamento es encontrar un archivo ELF de 32 bits ejecutable independientemente que solo rv32i instrucciones rv32i .

Sin embargo, el conjunto de instrucciones y extensiones se repondrán, ganarán impulso y aumentarán de peso.

Resumen y enlaces

Resultó ser una narración patética con sabor a historia personal. A veces técnico, a veces subjetivo. Sin embargo entusiasta y con un toque de entusiasmo.

Por mi parte, me interesa saber de usted: comentarios, impresiones, buenas palabras de despedida. Y para los más atrevidos: ayuda para apoyar el proyecto.

¿Está interesado en un formato tan narrativo y le gustaría continuar?

Cómo llegué a la especificación formal de un procesador RISC-V en F #