La verificación es el proceso de revisar, inspeccionar o probar el diseño del hardware para obtener el resultado deseado. Todo el proceso gira en torno a una pregunta: ¿la especificación coincide con la implementación? Esta pregunta debe hacerse durante todo el proceso de verificación.
Estructura del proceso de verificación
La estructura básica de cualquier proceso de verificación es la siguiente:
Considere el caso de RISC-V (pronunciado 'Risk-Five'). No se puede negar que RISC-V es un competidor fuerte y tiene un gran apoyo de la industria, por ejemplo, los eventos de RISC-V están atrayendo a más expositores. Incluso después de tener décadas de presencia en el mercado, falta la adopción de RISC-V como un núcleo integrado en dispositivos independientes.
Aún no se ha realizado ningún proceso de certificación y estandarización y no hay plug-and-play disponible en ningún punto de las pilas de hardware o software. Sin embargo, si volvemos atrás y revisamos el historial, este escenario es bastante similar al de Linux. Eventualmente, RISC-V también llegará al mercado masivo a través de la colaboración abierta entre los actores de la industria, ya sean grandes o pequeños.
A diferencia del software, no puede encontrar ningún núcleo de código abierto si está trabajando en un proyecto integrado. Todos hemos visto el cambio universal desencadenado por el código abierto en la industria del software. Con un objetivo idéntico, RISC-V pretende eliminar la influencia de la arquitectura patentada en el diseño del procesador. RISC-V tiene un potencial ilimitado para el crecimiento futuro, ya que ofrece un nuevo nivel de libertad de software y hardware en la arquitectura; como el software, uno no necesita depender de un solo proveedor.
Según Fundación RISC-V, "RISC-V es una arquitectura de conjunto de instrucciones (ISA) libre y abierta que permite una nueva era de innovación de procesadores a través de la colaboración de estándares abiertos". La Universidad de California, Berkeley, nombró lógicamente a la quinta arquitectura RISC clásica como RISC-V. Al reducir la necesidad de acercarse a la memoria externa para muchas de las tareas principales de la CPU, el RISC-V libre de regalías y no restrictivo reduce el uso de energía y aumenta la velocidad en gran medida. RISC-V es un ISA compacto, perfecto para aplicaciones integradas con mayor rendimiento y seguridad, incluidos los requisitos de bajo consumo.
Los primeros chips informáticos 'Made in India', los procesadores SHAKTI, basados en RISC-V ISA, están destinados a aplicaciones del mundo real y pueden ser adoptados libremente por las industrias (consulte beneficios de RISC-V para obtener más información). Huami, respaldado por Xiaomi, había lanzado Huangshan No. 1, un chipset portátil RISC-V, el año pasado. Otros ejemplos son Nvidia y Western Digital; estas empresas van a construir sus tarjetas gráficas y unidades de disco respectivamente, utilizando RISC-V.
La prueba y verificación es la tarea más destacada en el desarrollo de silicio y las plataformas RISC-V no son una excepción. Las herramientas y métodos de verificación líderes en la industria tendrán la ventaja para ofrecer soluciones basadas en RISC-V dentro de los criterios de tiempo y costo estipulados. La verificación formal ayuda a la industria a hacerlo; ayuda a descubrir errores que a menudo pasan desapercibidos con las pruebas tradicionales de verificación dirigida.
Sin embargo, existen muchos desafíos al realizar la verificación de RISC-V. El desafío más fundamental de verificar cualquier diseño es tener una mayor controlabilidad y observabilidad. Para eso, se debe generar un estímulo, que podría ser una estructura o algún comportamiento, para activar una línea de código específica. También se requiere generar un estímulo adicional para propagar la línea de código generada previamente a una salida donde se pueda observar. Agregamos afirmaciones, específicamente afirmaciones de bajo nivel, incrustadas dentro del diseño. Las afirmaciones también pueden ser útiles para identificar el buen comportamiento. Entonces, un verificador es útil para detectar resultados correctos o incorrectos.
Otro desafío importante asociado con RISC-V es la compatibilidad. Aunque ya existe una gran variedad de partes que proporcionan núcleos RISC-V, y este número puede aumentar considerablemente en el futuro previsible, no hay un solo equipo central que diseñe y verifique estos núcleos. Los proveedores de núcleos y los desarrolladores de SoC tienen que superar muchos desafíos para hacer diseños que sean compatibles entre sí, que cumplan con ISA y que tengan núcleos completamente verificados.
El desafío final en el que uno debe concentrarse es en las vulnerabilidades de seguridad, protección y confianza. Los diseños de núcleo (y SoC) deben examinarse en busca de todas estas susceptibilidades que podrían ser explotadas por alguien que desee tomar el control del sistema. Las implicaciones para aplicaciones como vehículos autónomos y militares/aeroespaciales ciertamente podrían ser terribles. Tanto los proveedores principales como los usuarios deben utilizar un proceso de verificación que detecte tales violaciones de la confianza y la seguridad.
Las posibilidades de cerrar esta brecha, aunque difíciles, no son una tarea imposible. La solución radica en la comprensión uniforme del problema. Las amenazas discutidas anteriormente conducen a una solución inevitable: verificación formal del diseño. La verificación formal es otro método de verificación, con el mismo objetivo de eliminar fallas de diseño. Utiliza herramientas formales y SystemVerilog Assertions (SVA). Valida o invalida los algoritmos previstos con respecto a una determinada especificación formal.
En primer lugar, la verificación formal no solo proporciona núcleos totalmente compatibles, sino que también identifica cualquier funcionalidad no deseada más allá de la especificación ISA. Esto detecta cualquier troyano de hardware, escanea el diseño y también lo protege de las vulnerabilidades de seguridad y confianza.
En segundo lugar, la seguridad es otro frente en el que ayuda la verificación formal; sopesa el diseño del núcleo y calcula las métricas de fallas y fallas requeridas por los estándares de seguridad. Las herramientas formales probarán no solo que el diseño hace lo que se especifica que haga, sino que también comprobarán que no hace lo que no se espera que haga y esto proporciona una mejor controlabilidad y observabilidad.
Además, la verificación formal es incluso mejor que la funcional. Uno tiene que generar un caso de prueba con controladores, monitores, modelos y verificadores mientras se realiza la verificación funcional. Además, se debe redactar una gran cantidad de código incluso antes de que le permita escribir su prueba inicial. Por el contrario, no existe el concepto de escribir casos de controlador, monitor y prueba en la verificación formal. La herramienta se encarga de generar todos los estímulos e informar si hay una falla; todo lo que necesita hacer es restringir las entradas adecuadamente y escribir fichas teniendo en cuenta la especificación de diseño.
Resumen
Para concluir, lo cierto es que verificar RISC-V seguramente tiene problemas complejos de controlabilidad y observabilidad, compatibilidad, además de vulnerabilidades de seguridad, protección y confianza. La verificación formal, con las ventajas discutidas anteriormente, es sin duda una mejora importante. Será una solución adecuada si la implementa el grupo adecuado de personas con el mayor cuidado: los problemas en cuestión se pueden mitigar en gran medida.
Generalmente se observa que la verificación formal, realizada por un tercero, es la mejor y la más útil para el crecimiento del ecosistema RISC-V. Esto ampliará el espacio para que múltiples proveedores principales conduzcan a una solución similar y con este RISC-V será un punto de inflexión para la industria de los semiconductores.
Para comenzar con la verificación RISC-V, ponte en contacto con nosotros.
