Modelado de componentes de hardware en Haskell | Defensa de Trabajo Especial

Día: viernes 28 de febrero de 2025

Hora: 10:00 h

Lugar: Aula Magna | FAMAF

Resumen: La especificación de componentes es una tarea fundamental en el diseño de hardware. Habitualmente esta se lleva a cabo a través de Lenguajes de Descripción de Hardware (HDL), como VHDL o Verilog, los cuales trabajan en el nivel de abstracción conocido como Register Transfer Level (RTL). Este nivel permite describir cómo los datos se mueven entre los registros y las operaciones que se les aplican en cada ciclo de reloj. Esto implica que al momento de desarrollar una descripción es necesario conocer en gran detalle la implementación del hardware. Sin embargo, a medida que los sistemas electrónicos se vuelven más complejos, las limitaciones de trabajar exclusivamente en este nivel se hacen evidentes, especialmente en términos de reutilización y verificación formal. Una alternativa, que es utilizada por el Centro de Supercómputo de Barcelona es el desarrollo de una librería de componentes parametrizables, la cual brinda componentes fácil de adaptar y testeados. La ventaja que esto brinda es reducir la reimplementación de componentes genéricos, y con ello las posibilidades de bugs. A pesar de eso sigue teniendo ciertas desventajas: es código RTL, por lo que puede resultar complicado entender qué hace un componente; las certezas que tenemos sobre los componentes de la librería no las tenemos sobre los componentes que nosotros formemos utilizando estos. Una solución a estos puntos resulta ser formalizar esta librería de componentes en un lenguaje que nos permita una mejor comprensión de la semántica de un componente y poder verificar que estos satisfagan ciertas propiedades. Este trabajo se enfoca en la investigación de lenguaje de diseño de hardware de alto nivel (HLHDL) como lo son Chisel, ReWire, Bluespec y Lava, examinando sus distintas características y enfoques. En particular, se explora cómo el paradigma funcional puede ofrecer nuevas alternativas en este campo. Además se realiza la implementación de un framework/dsl en Haskell que nos permite describir y simular componentes de hardware, considerando características necesarias para el modelado de una librería de componentes parametrizables. El objetivo del trabajo es proporcionar una visión integral sobre los lenguajes de especificación de hardware y explorar cómo el modelado funcional puede contribuir a una descripción más eficiente, abstracta y verificable de componentes de hardware.