Lenguajes y herramientas de especificación y verificación de sistemas


Hoy hemos tenido la primera sesión de esta asignatura troncal del máster en computación especialidad sistemas embebidos: M15: Lenguajes y herramientas de especificación y verificación de sistemas ( Periodo: 19 Nov. A 19 de Dic. 2008 ) El profesor, Eugenio Villar Bonet, nos ha informado de que vamos a tener un entorno virtual de aprendizaje en el Aula Virtual de la Universidad de Cantabria donde vamos a encontrar todo el material del curso.

El período de la asignatura se distribuye en 45 horas presenciales y 80 horas de trabajo del alumno (no presencial) Las 45 horas presenciales se distribuyen en 30 horas de seminario teórico con ejercicios propuestos (a realizar dentro de las 80 horas, supongo) y 15 horas de laboratorio. Las horas de laboratorio las da Fernando Herrera. Las horas teóricas las da Eugenio Villar. El horario de las teóricas de lunes a viernes de 17 a 20 horas. Vamos a tener un profesor visitante, Axel Jantsch, que va a impartir una parte del temario, en concreto los modelos de computación. Su parte será impartida en una semana de Febrero (10-15 horas)

La evaluación de la asignatura sigue las directrices innovadoras de Bolonia. El 50% de la calificación se deriva de la resolución de los ejercicios propuestos. La calificación se realiza por el método de evaluación colectiva. Los ejercicios se plantean a todos los alumnos pero se asigna a uno, que debe resolverlo y defender su solución ante el resto de los compañeros y profesor. Tras la presentación se abrirá un periodo de discusión. Al final el profesor dará una calificación y los compañeros otra. La nota final será la media de la nota del profesor y la media de la nota del resto de los compañeros. Para evitar suspicacias y asegurar una calificación justa de los compañeros (que idealmente deben juzgar la solución con conocimiento de causa y comparando con la propia) se utilizará un sistema mediante el cual la nota que individualmente emita cada compañero se comparará con la emitida por el profesor y si la diferencia es mayor que una cierta cantidad, la nota del alumno se descartará y se le penalizará con unas décimas en su nota final.

El otro 50% de la nota provendrá de la evaluación de las prácticas de laboratorio.

Introducción

En esta primera sesión teórica de 3 horas se ha dado una introducción general al tema del curso. Los objetivos del mismo han sido el objeto de las primeras transparencias. Debemos conocer los fundamentos de los lenguajes de especificación y verificación de sistemas embebidos “heterogéneos”, entendiendo por ese término sistemas que están compuestos por hardware y software muy interrelacionados. También aprenderemos a utilizar uno de los más utilizados en este momento en la industria y en la academia: SystemC (ver un guía del lenguaje en la red)

El resultado de la codificación de la especificación del sistema en un lenguaje como SystemC es un modelo ejecutable (mediante simulación) que permite validar y verificar la especificación (funcional y temporal) a diferentes niveles de abstracción. La simulación, no obstante, no es un método formal de análisis y por lo tanto hay que asegurar una cierta cobertura o soporte de verificación que acote el error cometido por la limitación de la simulación.

El modelo pues permite capturar las características funcionales y no funcionales del sistema y permite un análisis (MDA, Model Driven Analysis) y exploración del espacio de diseño (Model Drive Desingn)

(MP)SoC, el objetivo de diseño

Los sistemas objeto de análisis y diseño se denominan SoC. La antigua denominación de circuito electrónico ha quedado obsoleta por cuanto el avance de la tecnología de fabricación electrónica a permitido integrar en un solo chip un sistema completo. Por lo tanto la complejidad y la interacción entre los componentes ha aumentado y las prestaciones y restricciones funcionales y no funcionales deben ser modeladas con lenguajes formales potentes.

Ahora la amplitud de las decisiones tecnológicas a la hora de implementar las especificaciones de un sistema es inmensa: ASIC vs FPGA, analog vs digital, HW vs SW (la partición entre HW y SW en un proceso de co-diseño es fundamental), reuso de COTS vs diseño propio, comercial vs Open Source.

NOTA: Eugenio Villar preguntó cuáles eran los elementos hardware más reutilizados en la actualidad: processor cores (general and DSPs) p.e ARMs, memories, buses, …

Además existe un entorno muy competitivo en el que el margen comercial se reduce a la mínima expresión, el time-to-market es muy pequeño y el ciclo de vida de los productos es también reducido. Todo lo anterior lleva a una necesidad de adaptar los procesos de diseño para poder competir.

Las restricciones de diseño que se consideran son: funcionales, temporales, consumo de energía, fiabilidad, tamaño, costo, … que dan lugar a sistemas reactivos y de tiempo real.

Flujo de Diseño

Nos dieron una persectiva del diseño tradicional (se dispone/fija primero la plataforma hardware y se desarrolla posteriormente el software que corre sobre la misma, siguiendo un proceso de refinado/parcheado para cumplir con la funcionalidad y restricciones de la especificación), pasando por el diseño basado en plataformas (en el que existe una posibilidad de refinar la plataforma hardware que está basada en componentes que se pueden tunear) hasta llegar al momento actual en el que la empresa puede tener el control sobre todos los aspectos del sistema en lo que se denomina codiseño HW/SW:

> co-design HW/SW = requisitos -> diseño funcional -> especificación ejecutable incluyendo elementos funcionales y no funcionales (lenguaje de especificación simulable)* -> co-diseño (obtención de código HW + SW cosimulable) -> {síntesis (HW) Y compilación (SW)} -> integración.

*NOTA: que permite analizar explorar y verificar que la especificación es correcta y óptima …

En los estudios de grado se (supone que se) estudia del codiseño a la integración. En este estudio de posgrado (máster) se trata de los requisitos a la especificación.

Los lenguajes de diseño más utilizados son el C/C++/ADA en SW (no se menciona curiosamente el Java) y el VHDL/Verilog en HW. Recientemente estas dos visiones se han unido en lenguajes como SystemC o System Verilog capaces de realizar la cosimulación y luego refinarse (sintetizarse/compilarse) en ambos sentidos (HW y SW) hacia los lenguajes descritos.

Modelado vs Especificación

Una de las cuestiones en las que se detuvo Eugenio Villar y puso gran énfasis fue la distinción entre modelado y especificación.

La especificación es el punto de entrada del proceso de diseño. Tiene por objeto la captura y descripción de las restricciones y propiedades funcionales y no funcionales del sistema que se desea implementar. Es el primer peldaño de un camino vertical que continua con la síntesis/compilación (automático) o refinamiento (manual) hacia una especificación de más bajo nivel. Esta nueva especificación es otro punto de partida hacia la implementación final. La palabra clave de este proceso es que todo lo que se obtiene es sintetizable. Esto significa que hay un camino que va desde la especificación hasta la implementación.

Por contra el modelado (MDD, Model Driven Design) tiene por objeto capturar las propiedades funcionales y no funcionales conocidas de un sistema, al nivel de abstracción que se considere. Es el primer paso de un camino horizontal que continua con el análisis/simulación del modelo del que se obtienen unos resultados. A través de un proceso de refinamiento de modelos vertical se puede repetir el camino horizontal. Entre los resultados de diferentes niveles se tiene que dar una equivalencia que se valida mediante un proceso de verificación. Cada refinamiento implica un coste mayor del análisis/simulación y una mayor precisión. Al final hay que realizar una compleja transformación del modelo en un lenguaje de descripción para pasar del modelo analizable al código sintetizable.

NOTA 1: Por lo visto matlab/simulink se centra en el modelado y carece de la capacidad de pasarse a la síntesis/compilación.

NOTA 2: Yo considero aquí que el concepto de “sinteizable” puede aplicarse tanto al HW (su acepción original) como al SW. El resultado de la síntesis es una plataforma hardware y unos binarios software que corren en la plataforma y están perfectamente adaptados y optimizados para cumplir las especificaciones del sistema.

Clasificación de Sistemas

Se hizo una clasificación (creo que se mencionó que era de Petru Eles o Axel Jantsch) de los sistemas que se van a tratar en el curso. Por cierto que en la web de estos dos están las asignaturas que imparten con muchos temas que pueden estar incluidos en el presente curso. Están todas las presentaciones (he visto las de Petru) Sobretodo quiero destacar las asignaturas:

Nos pusieron un esquema es forma de árbol binario en la que siempre nos interesan las segunda rama (excepto en el caso de la división entre sistemas lineales y no lineales en el que interesan ambos)

La primera división es entre sistemas estáticos y dinámicos. La segunda división es entre variantes e invariantes en el tiempo. La tercera división es entre lineales y no lineales. La cuarta división es entre continuos y discretos. La quinta división es entre tiempo continuo y tiempo discreto. La sexta división es entre los dirigidos por eventos y los dirigidos por tiempo. La séptima división es entre deterministas y no deterministas.

NOTA 1: Los sistemas continuos de tiempo continuo son el objetivo de la extensión AMS de SystemC.

NOTA 2: La explicación de la distinción entre lso sistemas dirigidos por eventos y los dirigidos por tiempo está en un libro (no mencionó el título) de Petru Eles.

NOTA 3: Los sistemas no deterministas son muy útiles como demuestran los procesadores que optimizan la ejecución de instrucciones en sus pipelines con el método out-of-order execution.

6 comentarios en “Lenguajes y herramientas de especificación y verificación de sistemas

  1. Ha anotado algunas referencias bibliográficas importantes que se han mencionado (se encuentran en la guía de estudio del curso a la que todavía no he tenido acceso) Destacan los libros siguientes:

    Número: 180275
    Título: Design of hardware-software embedded systems / Eugenio Villar (ed.).
    Editorial: Santander : Servicio de Publicaciones de la Universidad de Cantabria, 2001.
    Descripción física: 173 p. ; 30 cm.
    ISBN: 84-8102-284-5
    Materias: Sistemas, Diseño de.
    Autor: Villar Bonet, Eugenio, ed. lit.
    IND B C61 35/35a

    Número: 208267
    Autor: Jantsch, Axel.
    Título: Modeling embedded systems and SoCs : concurrency and time in models of computation / Axel Jantsch.
    Editorial: San Francisco [etc.] : Morgan Kaufmann, cop. 2004.
    Descripción física: 351 p. ; 25 cm.
    Colección: The Morgan Kaufmann series in systems on silicon
    ISBN: 1-55860-925-3
    Materias: Tiempo Real. Circuitos Integrados — Diseño y Construcción.
    IND B C51 130/130a

    Número: 197776
    Título: System design with SystemC / Thorsten Grötker … [et al.].
    Editorial: Boston : Kluwer Academic Publishers, cop. 2002.
    Descripción física: 217 p. ; 25 cm.
    ISBN: 1-4020-7072-1
    Materias: Sistemas, Diseño de. C ++ (Lenguaje de Programación)
    Autor: Grötker, Thorsten
    IND M C61A 244

    Número: 204197
    Título: SystemC : methodologies and applications / edited by Wolfgang Müller, Wolfgang Rosenstiel and Jürgen Ruf.
    Editorial: Boston : Kluwer Academic Publishers, 2003.
    Descripción física: 349 p. ; 25 cm.
    Notas: Incluye colaboraciones de Fernando Herrera Casanueva, Pablo Pedro Sánchez Espeso, Víctor Manuel Fernández Solórzano, Eugenio Villar Bonet.
    ISBN: 1-4020-7479-4
    IND M C61A 250/250a

    Número: 251359
    Autor: Bergeron, Janick.
    Título: Writing testbenches using System Verilog / by Janick Bergeron.
    Editorial: New York : Springer, cop. 2006.
    Descripción física: 412 p. ; 24 cm.
    ISBN: 0-387-29221-7
    Materias: Circuitos Integrados Digitales.Verificación (Lógica) Lenguajes de Descripción de Hardware. Verilog (Lenguaje de Descripción de Hardware)
    IND B E25 29/ IND M E25 145b

    Número: 205373
    Autor: Bergeron, Janick.
    Título: Writing testbenches : functional verification of HDL models /Janick Bergeron.
    Edición: 2nd ed.
    Editorial: Boston [etc.] : Kluwer Academic Publishers, [2003]
    Descripción física: 475 p.
    ISBN: 1-4020-7401-8
    Materias: Circuitos Integrados Digitales. Verificación (Lógica) Lenguajes de Descripción de Hardware.
    IND M E25 145a

  2. Todavía no está disponible el entorno de aprendizaje online de la asignatura. Desconozco cómo entrar en el Aula Virtua. (probablemente voy a necesitar una cuenta de alumno o PDI …)

    No tengo los apuntes del tema 1 ni los enunciados de los dos primeros ejercicios propuestos de síntesis de comportamiento en VHDL de una convolución especificada en código C secuencial, con restricciones de disponibilidad de elementos hardware y con la condición de que el código resultante sea sintetizable.

    La estrategia más adecuada para resolver esos problemas, según nos contó Eugenio, es identificar la concurrencia en el código secuencial C (un C especial de sistemas embebidos) del enunciado y paralelizarlo (quitando los bucles, por ejemplo), analizar las restricciones temporales y codificar el comportamiento en VHDL teniendo en cuenta los recursos de los que se disponen.

    El proceso descrito en la nota anterior se parece mucho al proceso que seguían los de IMEC con su Clean C para obtener código analizable y al proceso de synfora para poder traducir los algoritmos C en hardware basado en componentes (correct-by-construction)

  3. El curso presupone unos conocimientos adquiridos en los cursos de grado de electrónica digital. En concreto un conocimiento de síntesis de comportamiento en lenguaje VHDL y su síntesis RTL, netlist y celdas. Los que no hemos cursado dicho grado tenemos que buscarnos la vida y adquirir esos conocimientos.

    Aquí van unos enlaces que he encontrado sobre VHDL:

    VHDL Tutorial
    HDL Tutorial: Learn by Example — by Weijun Zhang
    Lenguajes de Descripción Hardware: VHDL
    – DOULOS: The Designer’s Guide to VHDL
    – DOULOS: The Designer’s Guide to Verilog

    NOTA: Eugenio Villar indica que en el mundo de la industria se usa ampliamente Verilog y System Verilog.

  4. Hola yerart!!

    me llamo benet soy ingeniero técnico de telecomunicaciones y estoy cursando Ingenieria electronica en la Universitat autonoma de Barcelona.

    el probelma de esta carrera aqui es que es muy cientifica y poco tecnica en ingenieria. quiero decir que machacamos mucho el estudio del transitor más que otra cosa.

    a lo que iva!! pero aun así, estoy interesado en los sistemas empotrados. Y querría preguntarte sobre cursos o postgrados, que se hagan por aqui en Cataluña!! sobre este tema. y sino tambien enfocarme que pasos seguir para poder llegar a disñar sistmeas empotrados

    Lo maximo que he dado en las dos carreras ha sido ensamblador para micros (motorola) y el disño digital en VHDL con FPGA de altera (diseñamos un microprocesador bastante simple, pero bastante instructivo). el año que viene seguire con una assignatura de sistemas electronicos que es equivalente a diseño coHardware-software!!

    bueno gracias

    recomiendame!!

Responder

Introduce tus datos o haz clic en un icono para iniciar sesión:

Logo de WordPress.com

Estás comentando usando tu cuenta de WordPress.com. Cerrar sesión / Cambiar )

Imagen de Twitter

Estás comentando usando tu cuenta de Twitter. Cerrar sesión / Cambiar )

Foto de Facebook

Estás comentando usando tu cuenta de Facebook. Cerrar sesión / Cambiar )

Google+ photo

Estás comentando usando tu cuenta de Google+. Cerrar sesión / Cambiar )

Conectando a %s