Verificación de Hardware ASIC FPGA De la Complejidad al Dominio — Versión Parcial de Cortesía.pdf

Verificación de Hardware ASIC/FPGA:
De la Complejidad al Dominio

Por
Carmen Silva H.
Editado por María de Lourdes Scoppetta Silva

Verificación de Hardware ASIC/FPGA:
De la Complejidad al Dominio

Copyright © 2025 por Carmen Silva H.
Todos los derechos reservados. Ninguna parte de este libro puede ser reproducida o
transmitida de forma alguna o por ningún medio, electrónico o mecánico, incluyendo
fotocopiado, grabación o por medio de sistemas de almacenamiento y recuperación de
información, sin permiso escrito del propietario de los derechos de autor.
Editora: María de Lourdes Scoppetta Silva
Términos y condiciones

Verificación de Hardware ASIC/FPGA:
De la Complejidad al Dominio
Duración Total Estimada: Entre 25 y 45 horas de lectura.
Justificación de la Estimación:
●Densidad Técnica: El material no es de lectura rápida. Cada concepto, técnica y
ejemplo requerirá tiempo para ser asimilado.
●Profundidad: El esquema indica un tratamiento detallado de cada tema, y los
ejemplos añadirán una capa adicional de tiempo de estudio.
●Nivel del Lector: Aunque la audiencia es técnica, aprender o revisar
metodologías avanzadas como FV o aspectos detallados de seguridad a bajo
nivel no es trivial.
●Ejemplos: La inclusión de 1-3 ejemplos por sección/subtema es muy valiosa,
pero si estos ejemplos incluyen código (SVA, SystemVerilog, etc.), diagramas de
flujo complejos o trazas de simulación/formal, su análisis detallado consumirá
una parte significativa del tiempo total.
Este rango asume una lectura concentrada con pausas para reflexión y posiblemente
revisitar secciones. Para un lector con un conocimiento muy sólido que lo use como
referencia rápida, el tiempo podría ser menor. Para alguien que se inicie en varios de
los temas, o que decida trabajar activamente con los ejemplos, la duración podría
exceder este rango.
Por lo tanto, 25 a 45 horas representa una estimación para una lectura comprensiva
por parte de la audiencia objetivo.
La audiencia objetivo principal:

1.Ingenieros de Verificación (Verification Engineers): Especialmente aquellos que trabajan
o aspiran a trabajar con metodologías avanzadas como la Verificación Formal (FV) y la
Verificación Basada en Cobertura/Aleatoriedad Restringida (CDV/CRV con UVM).
Necesitan profundizar en cómo aplicar estas técnicas a problemas complejos de
corrección y seguridad a bajo nivel.
2.Ingenieros de Diseño de Hardware (Hardware Design Engineers): Aquellos que diseñan
ASICs o FPGAs a nivel RTL o superior, pero que necesitan comprender los desafíos de
la verificación de sus diseños en etapas posteriores y cómo diseñar pensando en la
verificabilidad y la seguridad ("Design for Verification" - DfV y "Design for Security" -
DfS).

3.Arquitectos de Hardware (Hardware Architects): Profesionales que definen la estructura
general del sistema y sus componentes. Deben conocer las implicaciones de sus
decisiones arquitectónicas en la verificabilidad y seguridad a bajo nivel.
4.Especialistas en Seguridad de Hardware (Hardware Security Specialists): Ingenieros o
investigadores enfocados específicamente en identificar y mitigar vulnerabilidades en
hardware. El ebook les proporcionaría un entendimiento de cómo las metodologías de
verificación pueden ser herramientas poderosas en su campo. 5.Investigadores y Académicos: Personas en el ámbito universitario o de investigación
que estudian nuevas técnicas de verificación formal, simulación avanzada, o seguridad
de hardware a bajo nivel.
6.Estudiantes de Posgrado (Graduate Students): Estudiantes de ingeniería eléctrica,
electrónica o ciencias de la computación con un enfoque en diseño o verificación de
VLSI/Hardware, que buscan un recurso técnico detallado sobre estas áreas
especializadas. En esencia, la audiencia son profesionales y estudiantes avanzados en el campo del diseño y
la verificación de circuitos integrados que necesitan adquirir conocimientos profundos y
prácticos sobre cómo asegurar la corrección funcional y la robustez contra amenazas de
seguridad en las implementaciones de hardware a bajo nivel.
Objetivo General: Dotar al lector con un entendimiento profundo y la capacidad de aplicar
metodologías avanzadas de verificación formal y de diseño (basada en simulación) para
garantizar la corrección funcional, la fiabilidad y la seguridad de diseños de hardware
modernos (ASICs/FPGAs) a bajo nivel (principalmente RTL y nivel de compuertas).
En términos más concretos, al finalizar la lectura, el lector deberá ser capaz de:
1.Comprender la criticidad de la verificación a bajo nivel y los desafíos inherentes a la
complejidad y las amenazas de seguridad actuales.
2.Analizar las bases teóricas y prácticas de la Verificación Formal, incluyendo lenguajes
de propiedades y técnicas (Model Checking, Equivalence Checking), y discernir cuándo
y cómo aplicarla eficazmente.
3.Dominar las metodologías de Verificación Basada en Simulación avanzadas (como UVM
con CRV/CDV) y comprender su aplicación específica para la verificación exhaustiva a
bajo nivel, incluyendo la Simulación a Nivel de Compuertas (GLS).
4.Identificar las principales vulnerabilidades de seguridad del hardware a bajo nivel
(Hardware Trojans, Side Channels, etc.) y conocer las técnicas específicas, tanto
formales como basadas en simulación, para su detección y verificación.
5.Considerar cómo las técnicas de verificación se aplican o interactúan con otros aspectos
críticos a bajo nivel, como el timing, la potencia y la señal mixta.
6.Integrar y gestionar eficazmente las diferentes metodologías de verificación en un flujo
de trabajo coherente para lograr un sign-off riguroso del diseño.
7.Estar familiarizado con las tendencias actuales y futuras en el campo de la verificación
de hardware.

En síntesis, el objetivo es transformar al lector en un especialista más competente, equipado
con las herramientas conceptuales y prácticas necesarias para abordar los complejos retos de
asegurar la calidad y la seguridad en las capas fundamentales de los diseños de circuitos
integrados.
Sitio web: Tech&Ebooks
Email: [email protected]

Índice
Índice
Prefacio
La creciente complejidad de los ASICs/FPGAs.
La importancia crítica de la corrección funcional.
La emergencia de las amenazas de seguridad a nivel de hardware.
El papel indispensable de la Verificación Formal y de Diseño avanzada.
Audiencia a la que se dirige el libro.
Capítulo 1: Introducción: El Imperativo de la Verificación de Hardware a Bajo Nivel
1.1 El Desafío de la Complejidad en Diseños Modernos
● Escalado Tecnológico (Moore's Law y más allá).
● Integración de IP de terceros y sus riesgos.
● Diseños heterogéneos (Digital, Analógico, Mixto).
● [Desarrollo del Ejemplo para 1.1]
1.2 ¿Qué Implica "Bajo Nivel" en la Verificación de Hardware?
● Desde la Descripción RTL (Register-Transfer Level).
● Pasando por la Netlist de Compuertas (Gate-Level).
● Consideraciones post-layout (Timing, Power, Efectos Físicos).
● [Desarrollo del Ejemplo para 1.2]
1.3 ¿Por Qué la Verificación Tradicional es Insuficiente?
● Limitaciones de la simulación dirigida (Test Vectors específicos).
● El problema del espacio de estados (State Space Explosion).
● La dificultad de identificar errores o vulnerabilidades sutiles y de rara ocurrencia.
● [Desarrollo del Ejemplo para 1.3]
1.4 La Convergencia de la Corrección Funcional y la Seguridad
● Errores funcionales que pueden ser explotados como vulnerabilidades de seguridad.
● Vulnerabilidades de seguridad que impactan la funcionalidad (Ej: Hardware Trojans).
● La necesidad de un enfoque unificado.
● [Desarrollo del Ejemplo para 1.4]
Capítulo 2: Fundamentos de la Verificación de Hardware y los Desafíos del Bajo Nivel
2.1 El Proceso de Diseño y Verificación de ASICs/FPGAs
● El Proceso de Diseño y Verificación de ASICs/FPGAs.
● Posicionamiento de las diferentes etapas de verificación.
● El costo de los errores en etapas tardías (Respines).
● [Desarrollo del Ejemplo para 2.1]
2.2 Tipos de Errores de Diseño Comunes
● Errores funcionales (Lógica incorrecta).
● Violaciones de timing (Setup/Hold violations, Clock Domain Crossing - CDC).
● Problemas de potencia (Glitches, IR drop, Power sequencing).
● Vulnerabilidades de seguridad (Hardware Trojans, Backdoors, Side Channels).

2.3 Desafíos Específicos de la Verificación a Nivel RTL
● Manejo de la concurrencia.
● Verificación de Interfaces y Protocolos complejos.
● Asegurar la resetabilidad correcta.
2.4 Desafíos Específicos de la Verificación a Nivel de Compuertas (Gate-Level)
● Impacto de la síntesis y optimizaciones.
● Verificación con Información de Timing e Interconexiones (SDF).
● Manejo de Señales Tri-estado y X-propagation.
● Consideración de Efectos Físicos a nivel de Compuertas (revisitando).
Capítulo 3: Verificación Formal: Probanza Matemática de la Corrección
3.1 Introducción a la Verificación Formal
● ¿Qué es la Verificación Formal?
● Contraste con la verificación basada en simulación (Validación por ejemplos).
● Ventajas: Cobertura completa del espacio de estados (en algunos casos), hallazgo de
bugs profundos.
● Limitaciones: Escalabilidad, requerimiento de conocimiento experto, aplicabilidad.
● [Desarrollo del Ejemplo para 3.1]
3.2 Conceptos Clave de la Verificación Formal
● Modelos formales del diseño.
● Propiedades a verificar (Assertions, Assumptions, Cover Properties).
● El concepto de "espacio de estados" y "alcanzabilidad".
● Invariantes.
Apéndices
A.1 Glosario de Términos
Acerca de la Autora
Conclusión Parcial

Prefacio
La era digital contemporánea se cimenta sobre la omnipresencia de los circuitos
integrados, el corazón de la vasta mayoría de los sistemas electrónicos que definen
nuestra tecnología, desde dispositivos personales hasta infraestructuras críticas y
sistemas de inteligencia artificial. El diseño y la fabricación de estos componentes,
materializados como ASICs (Application-Specific Integrated Circuits) y FPGAs
(Field-Programmable Gate Arrays), representan una de las disciplinas de ingeniería
más sofisticadas y de rápida evolución. Este dinamismo trae consigo desafíos sin
precedentes, particularmente en lo referente a la garantía de su correcto
funcionamiento y su resistencia frente a amenazas adversarias.
La creciente complejidad de los ASICs/FPGAs.
La Ley de Moore continúa impulsando una integración cada vez mayor, permitiendo
que miles de millones de transistores residan en un único chip. Esta escalada ha
llevado a diseños masivamente complejos, que a menudo integran múltiples núcleos de
procesamiento, aceleradores especializados, interfaces de alta velocidad y vastas
cantidades de memoria en un solo sistema (SoC - System-on-Chip). Adicionalmente, la
adopción de nodos de proceso avanzados introduce nuevos fenómenos físicos y
variabilidad. Los diseños modernos frecuentemente incorporan arquitecturas
heterogéneas, con múltiples dominios de reloj y potencia, y la integración de propiedad
intelectual (IP) de terceros, cuya complejidad interna puede ser considerable. Esta
intrincada interconexión y la concurrencia inherente crean un vasto y complejo espacio
de estados de operación, cuya validación representa una tarea monumental.
La importancia crítica de la corrección funcional.
Asegurar que un diseño de hardware se comporte exactamente como se especifica es
de importancia capital. Un error funcional, por mínimo que sea a nivel de
implementación, puede tener consecuencias catastróficas. En el mejor de los casos, un
fallo detectado tarde en el ciclo de diseño puede requerir un "respin" de silicio,
implicando costos multimillonarios, retrasos significativos en la salida al mercado y una
potencial pérdida de competitividad. En el peor de los casos, un error no detectado
puede llevar a fallos en sistemas desplegados en aplicaciones críticas como la
automoción (sistemas de conducción autónoma), la aviónica, dispositivos médicos o
infraestructura de comunicaciones, poniendo en riesgo vidas humanas o causando
pérdidas económicas masivas. Los métodos de verificación tradicionales, basados
puramente en simulación con vectores de prueba limitados, son inherentemente
incapaces de ejercer completamente el espacio de estados de diseños complejos,

dejando lagunas donde los errores pueden acechar sin ser detectados.
La emergencia de las amenazas de seguridad a nivel de
hardware.
Históricamente, la seguridad de los sistemas electrónicos se ha enfocado
primordialmente en la capa de software y red. Sin embargo, se ha reconocido cada vez
más que si la base de hardware subyacente está comprometida, las medidas de
seguridad en capas superiores pueden ser ineficaces. Han surgido y se consideran
activamente nuevas amenazas que atacan directamente el hardware a bajo nivel. Estas
incluyen la inserción maliciosa de Hardware Trojans durante el diseño o la fabricación,
y los ataques de canal lateral (Side-Channel Attacks) que aprovechan las emanaciones
físicas del dispositivo (consumo de potencia, timing, emisiones electromagnéticas) para
inferir información secreta (como claves criptográficas). Examinar estas
vulnerabilidades requiere un conocimiento detallado de la implementación física y
lógica del diseño, y las técnicas de verificación tradicionales no fueron concebidas para
identificar este tipo de riesgos maliciosos.
El papel indispensable de la Verificación Formal y de Diseño
avanzada.
Ante este panorama de complejidad sin precedentes, la criticidad de la corrección y la
amenaza latente de la inseguridad, las metodologías de verificación han tenido que
evolucionar drásticamente. La Verificación Formal (FV) se presenta como una
herramienta poderosa, ofreciendo la capacidad, bajo ciertas condiciones, de demostrar
matemáticamente que ciertas propiedades deseadas son siempre verdaderas, o que
propiedades indeseadas son siempre falsas, cubriendo así la totalidad o una parte
significativa del espacio de estados, algo inalcanzable con simulación. Paralelamente,
la Verificación de Diseño (DV) basada en simulación ha avanzado enormemente con
metodologías como UVM, la Verificación Aleatoria Restringida (CRV) y la Verificación
Dirigida por Cobertura (CDV), permitiendo la validación de comportamientos complejos
a nivel de sistema y la búsqueda inteligente de casos de esquina difíciles de prever.
Estas dos aproximaciones no son mutuamente excluyentes, sino complementarias,
volviéndose indispensables en conjunto para abordar los desafíos de corrección y,
crecientemente, de seguridad a nivel de RTL y compuertas.
Audiencia a la que se dirige el libro.
Este libro ha sido concebido como una guía técnica y divulgativa para ingenieros de
diseño y verificación de ASICs y FPGAs, arquitectos de hardware, especialistas en

seguridad de hardware, investigadores y estudiantes avanzados en el campo. Se
asume que el lector posee un conocimiento fundamental de diseño de hardware digital
(lenguajes HDL como Verilog/SystemVerilog o VHDL) y conceptos básicos de
verificación. El texto busca presentar las metodologías, técnicas y enfoques avanzados
necesarios para analizar y asegurar la corrección funcional y la seguridad de los
diseños de hardware en sus niveles más bajos de abstracción, proporcionando el
conocimiento esencial para enfrentar los retos de la industria moderna del silicio.

Capítulo 1: Introducción: El Imperativo de la
Verificación de Hardware a Bajo Nivel
La fiabilidad y seguridad de los sistemas electrónicos modernos dependen fundamentalmente
de la corrección de su hardware subyacente. En un mundo cada vez más interconectado y
dependiente de la tecnología digital, la verificación de diseños de circuitos integrados,
especialmente a bajo nivel de abstracción, ha pasado de ser una etapa importante a
convertirse en un imperativo crítico. Este capítulo inicial sitúa al lector en el contexto actual del
diseño de hardware, presentando los desafíos fundamentales que hacen de la verificación un
campo de estudio y práctica tan vital, y sentando las bases para comprender por qué se
requieren metodologías avanzadas.

1.1 El Desafío de la Complejidad en Diseños Modernos
La complejidad es, sin duda, el factor dominante que impulsa la dificultad en la verificación de
hardware hoy en día. Los chips han dejado de ser simples circuitos con funciones discretas
para convertirse en sistemas completos en sí mismos, integrando una vasta cantidad de
funcionalidades y operando bajo diversas condiciones. Comprender la naturaleza de esta
complejidad es el primer paso para apreciar los retos que presenta la verificación,
particularmente en las etapas de implementación de bajo nivel, donde los detalles finos tienen
un impacto crítico. ●Escalado Tecnológico (Moore's Law y más allá).
Durante décadas, la industria de semiconductores ha sido testigo de un crecimiento
exponencial en la densidad de transistores en un chip, un fenómeno a menudo asociado con la
Ley de Moore. Esta tendencia ha permitido la integración de funcionalidades cada vez más
sofisticadas, desde procesadores multinúcleo de alto rendimiento y unidades de procesamiento
gráfico (GPUs) hasta aceleradores de inteligencia artificial (IA), subsistemas de comunicación
de última generación (5G, Wi-Fi 6E), y vastas cantidades de memoria integrada. Todo esto
reside dentro de un área de silicio limitada, lo que lleva a densidades de transistores
asombrosas. Sin embargo, a medida que las características físicas de los transistores se
reducen a escalas nanométricas (por ejemplo, 7nm, 5nm, 3nm), surgen nuevos y difíciles
desafíos que van "más allá de Moore". Los efectos físicos a esta escala, como la variabilidad
del proceso de fabricación (que causa diferencias significativas en las características de
transistores aparentemente idénticos), la fuga de corriente (subthreshold leakage), el
acoplamiento entre interconexiones (crosstalk) y los efectos cuánticos, se vuelven más
pronunciados y menos predecibles. Estos fenómenos pueden afectar de manera significativa el
comportamiento funcional y, especialmente, el timing del circuito, a menudo de formas sutiles y
dependientes del contexto operativo (temperatura, voltaje de alimentación, patrones de
actividad). Verificar que el diseño funcione correctamente y de manera fiable bajo todas las
condiciones esperadas, teniendo en cuenta esta variabilidad física, impone exigencias
extremas a las metodologías de verificación. Además, el enfoque actual también considera la
integración tridimensional (3D stacking) de chips o "chiplets" interconectados con alta densidad
(como tecnologías de interconexión 2.5D/3D), llevando la complejidad no solo al plano 2D, sino
a arquitecturas multicapa y multisistema que presentan nuevos desafíos de verificación
relacionados con la disipación térmica, la integridad de la señal a través de las interconexiones
verticales (TSVs) y la gestión de la comunicación entre capas.

●Integración de IP de terceros y sus riesgos.
Para gestionar la abrumadora complejidad del diseño de chips modernos y acelerar
drásticamente el tiempo de salida al mercado, los diseñadores recurren cada vez más a la
reutilización extensiva de bloques de propiedad intelectual (IP) preexistentes. Estos bloques
pueden ser complejos en sí mismos, abarcando desde núcleos de procesador estándar (como

ARM o RISC-V), controladores de interfaz (USB, PCIe, Ethernet), hasta bloques de memoria,
periféricos y subsistemas especializados. La IP puede provenir de diferentes fuentes: equipos
internos dentro de la misma empresa, proveedores externos especializados (comerciales) o
comunidades de código abierto. Si bien la integración de IP permite a los equipos concentrarse
en el desarrollo del "pegamento" y la innovación central de su producto, así como reducir los
costos de diseño desde cero, introduce nuevos y significativos vectores de riesgo en el proceso
de verificación a bajo nivel. A menudo, el equipo de diseño que integra la IP tiene una
visibilidad limitada o incompleta de sus detalles internos de implementación ("caja negra"). Esto
dificulta enormemente la verificación exhaustiva de la integración correcta de la IP con el resto
del diseño del SoC (por ejemplo, asegurar que se adhieren estrictamente a los protocolos de
interfaz, que las restricciones de timing a través de los límites de la IP se cumplen en todos los
modos de operación, o que la configuración de la IP es la esperada). Además de los errores
funcionales no intencionados dentro de la propia IP o en su integración, el riesgo de seguridad
asociado a la IP, especialmente si proviene de fuentes no completamente confiables, es una
preocupación creciente. Existe la posibilidad, difícil de descartar sin una verificación rigurosa,
de que la IP contenga funcionalidades maliciosas o vulnerabilidades no documentadas (como
Hardware Trojans o backdoors) insertadas deliberadamente. Presentan un desafío de
verificación particularmente espinoso debido a su naturaleza oculta y a menudo dependiente de
triggers complejos o de rara ocurrencia, que son extremadamente difíciles de detectar sin
visibilidad del código fuente a bajo nivel o la aplicación de técnicas de análisis especializadas.

●Diseños heterogéneos (Digital, Analógico, Mixto).
Los sistemas en chip modernos rara vez son puramente digitales. La integración de
componentes analógicos y de señal mixta es cada vez más común para interactuar con el
mundo real. Esto incluye bloques como convertidores de datos (ADCs para digitalizar señales
del mundo real, DACs para convertir datos digitales a señales analógicas), lazos de fase
cerrada (PLLs) para generar y gestionar relojes, interfaces de radiofrecuencia (RF), sensores y
complejos sistemas de gestión de potencia analógica. La verificación de estos sistemas
presenta un desafío significativo porque los bloques digitales y analógicos operan sobre
principios físicos diferentes y se modelan y simulan utilizando herramientas y metodologías
fundamentalmente distintas (simuladores HDL como Verilog/SystemVerilog para digital,
simuladores SPICE o Verilog-AMS para analógico y señal mixta). Verificar correctamente los
puntos de interacción entre estos dominios (interfaz analógico-digital) requiere técnicas de
cosimulación y modelado precisas para asegurar que las señales cruzan el dominio de manera
coherente y predecible. Además, la integración de componentes analógicos es a menudo la
fuente de múltiples dominios de reloj asíncronos dentro del chip digital, generados por PLLs o
recibidos de fuentes externas. Asegurar la integridad de los datos y la robustez del sistema
cuando la información cruza estos límites de reloj (Clock Domain Crossing - CDC) es una de las
tareas de verificación más críticas y propensas a errores a bajo nivel, requiriendo análisis
estáticos y, cada vez más, verificación formal para descartar la posibilidad de metaestabilidad o
pérdida de datos. Similarmente, los complejos esquemas de gestión de energía, a menudo
orquestados por lógica digital pero ejecutados por bloques analógicos/mixtos (regualdores de

voltaje, power gating), introducen múltiples dominios de potencia que pueden activarse y
desactivarse dinámicamente. La verificación de la corrección de las transiciones entre estados
de potencia, la retención de datos en dominios apagados, el aislamiento adecuado y la
prevención de glitches o comportamientos inesperados durante estos cambios (Power Domain
Crossing - PDC) requiere metodologías de verificación con conciencia de potencia, como la
simulación utilizando formatos estándar como UPF/CPF.

●[Desarrollo del Ejemplo para 1.1]
Para ilustrar el desafío de la complejidad en diseños modernos a bajo nivel, consideremos un
ejemplo de un Sistema en Chip (SoC) hipotético diseñado para una aplicación de
procesamiento de datos en el borde de la red. Este SoC podría incluir los siguientes
componentes, integrados a partir de diversas fuentes de IP y diseñados en nodos tecnológicos
avanzados:
●Un core de procesador de aplicación multinúcleo (IP de terceros comercial).
●Un acelerador de procesamiento de señal digital (DSP) personalizado diseñado
internamente.
●Un controlador de memoria DDR (IP de terceros) con una interfaz de alta velocidad.
●Un subsistema de red (IP de código abierto) que incluye interfaces Ethernet.
●Un subsistema de gestión de energía con múltiples dominios de voltaje y capacidad
de apagar selectivamente partes del chip (diseño mixto analógico/digital).
●Varios dominios de reloj generados por PLLs (bloques analógicos/mixtos), operando a
diferentes frecuencias y fases para el procesador, el DSP, la memoria y las interfaces de
red.
●Un bus de interconexión complejo (por ejemplo, basado en AXI) que conecta todos
estos bloques, manejando transferencias de datos concurrentes y asegurando la
coherencia de la caché entre los cores y los aceleradores.
¿Cómo esta complejidad afecta la verificación a bajo nivel?
1.Interacciones entre IPs: Verificar que el procesador (IP1) pueda comunicarse
correctamente con el acelerador DSP (diseño interno) a través del bus AXI (IP de
terceros) mientras accede a la memoria DDR (IP4) es un desafío multifacético. Requiere
verificar que los protocolos AXI se respeten estrictamente por todos los actores (un
problema de RTL/Gate-Level), que el timing de las señales a través de los límites de la
IP sea correcto (un problema post-layout/timing), y que las interacciones concurrentes
bajo alta carga no causen deadlocks o pérdida de datos (un problema de RTL/funcional
complejo).
2.Gestión de Dominios de Reloj (CDC): El core del procesador puede operar a una
frecuencia, el DSP a otra, la memoria DDR a una tercera y las interfaces de red a una
cuarta, todas derivadas de diferentes PLLs. La transferencia de datos entre el core y el

controlador DDR implica cruzar dominios de reloj asíncronos. Verificar la lógica de
sincronización (synchronizers) a bajo nivel (RTL) es crítico para prevenir la
metaestabilidad, que puede causar fallos arbitrarios y difíciles de reproducir. El análisis
formal es a menudo la única manera de garantizar que la lógica CDC está libre de fallos. 3.Gestión de Dominios de Potencia (PDC): El subsistema de gestión de energía puede
permitir apagar el core del procesador o el acelerador DSP cuando no están en uso
para ahorrar energía. Verificar que el estado (registros) de estos bloques se guarda
correctamente antes de apagar, que el aislamiento de señales es efectivo durante el
estado apagado, que el encendido ocurre sin fallos (glitches) y que la coherencia de la
caché se mantiene a pesar de los ciclos de encendido/apagado (un problema
funcional/power-aware a bajo nivel) es extremadamente complejo. Requiere simulación
con conciencia de potencia (UPF/CPF) y puede beneficiarse de análisis formales de las
propiedades de potencia.
4.Errores Sutiles en Nodos Avanzados: Incluso si cada bloque individual parece
funcionar correctamente en aislamiento, las interacciones a alta velocidad y las
variaciones a nivel de silicio en un nodo avanzado pueden causar problemas. Un
pequeño retraso adicional en una ruta crítica debido a la variabilidad del proceso o al
acoplamiento (crosstalk) post-layout podría violar un requisito de setup/hold, llevando a
un error funcional que solo se manifiesta en ciertas unidades fabricadas o bajo ciertas
condiciones ambientales. Verificar esto requiere GLS con anotaciones SDF precisas o
técnicas formales que consideren timing (si son aplicables).
5.Riesgos de Seguridad en IPs: Si el subsistema de red o el controlador DDR contienen
un Hardware Trojan incrustado en su RTL o netlist (quizás insertado en la cadena de
suministro de la IP), podría ser extremadamente difícil de detectar. Este Troyano podría
estar diseñado para activarse solo cuando el procesador realiza una operación de red
inusual y el chip está en un estado de bajo consumo particular (combinando
complejidad funcional, de dominio de potencia y de IP), fugando información a través de
la interfaz de red. Verificar la ausencia de tales amenazas requiere técnicas
especializadas que van más allá de la verificación funcional típica.
Este ejemplo multidimensional ilustra cómo la combinación del escalado tecnológico, la
integración de IP de diversas fuentes y la heterogeneidad de los diseños modernos crea un
espacio de verificación vasto e interconectado donde los fallos a bajo nivel son probables y
difíciles de identificar sin metodologías avanzación capaces de abordar esta complejidad
interdominio y de diferentes niveles de abstracción.

1.2 ¿Qué Implica "Bajo Nivel" en la Verificación de Hardware?
Cuando se habla de verificación de hardware "a bajo nivel", nos referimos típicamente a las
etapas del flujo de diseño que están más cerca de la implementación física del circuito
integrado, es decir, más allá del nivel de comportamiento o algoritmo puro. Estas etapas son
cruciales porque es donde la descripción abstracta del diseño se transforma en una estructura

que eventualmente será fabricada en silicio. Los desafíos de verificación en estos niveles son
distintos a los de etapas de mayor abstracción y requieren técnicas especializadas, ya que se
considera la estructura lógica real y, posteriormente, su plasmación física. Generalmente, se
consideran tres niveles principales dentro de este espectro de bajo nivel, cada uno con sus
particularidades de verificación.

●Desde la Descripción RTL (Register-Transfer Level).
El Nivel de Transferencia de Registros (RTL) es el punto de partida fundamental para la
implementación detallada de la lógica digital y la primera representación del diseño que es
directamente sintetizable. En RTL, el diseño se representa utilizando un Lenguaje de
Descripción de Hardware (HDL) como Verilog, SystemVerilog o VHDL, describiendo el circuito
en términos de registros (elementos de almacenamiento de estado como flip-flops y memorias)
y la lógica combinacional que define cómo los datos se mueven (transfieren) entre estos
registros, así como las operaciones lógicas y aritméticas que se realizan. Este nivel de
abstracción es donde el comportamiento funcional y la estructura del diseño se concretan de
manera detallada. La verificación en RTL es la etapa principal y más extensa para validar la
corrección funcional del diseño antes de cualquier transformación estructural (como la síntesis).
En este nivel, los ingenieros verifican la lógica de control implementada, asegurando que las
máquinas de estados finitos (FSMs) operan correctamente en todas las secuencias posibles,
que las rutas de datos (datapaths) realizan las transformaciones de datos esperadas sin errores

de precisión o desbordamiento, que las interfaces de comunicación se adhieren rigurosamente
a sus protocolos (handshaking, formatos de datos, etc.), y que la lógica de control coordina
adecuadamente todas las operaciones concurrentes entre diferentes partes del diseño. Los
errores lógicos descubiertos en RTL son los más fáciles y económicos de corregir, ya que solo
requieren modificaciones en el código fuente del HDL. Sin embargo, la complejidad inherente
de los diseños modernos, con miles o millones de líneas de código RTL, hace que asegurar
una cobertura completa de todos los posibles escenarios y estados funcionales sea un desafío
formidable incluso en esta etapa relativamente temprana del flujo de bajo nivel.

●Pasando por la Netlist de Compuertas (Gate-Level).
La Netlist de Compuertas (Gate-Level Netlist) es el resultado del proceso de síntesis lógica,
donde la descripción RTL abstracta se traduce automáticamente o "mapea" a una interconexión
de celdas lógicas básicas y secuenciales (como compuertas AND, OR, inversores, flip-flops,
celdas de memoria, buffers, etc.) seleccionadas de una biblioteca de tecnología de fabricación
específica. Este nivel de abstracción describe el diseño en términos de los elementos físicos
lógicos fundamentales y cómo están interconectados. La verificación a nivel de compuertas es
crucial para confirmar que el proceso de síntesis, que a menudo realiza optimizaciones
complejas (reducción de lógica, reestructuración, inserción de buffers, diseño de árboles de
reloj y reset), no ha introducido errores funcionales ni ha alterado el comportamiento
especificado en RTL. La herramienta principal para esta tarea es la Verificación de Equivalencia
Formal (Formal Equivalence Checking - FEC), que realiza una comparación matemática
rigurosa entre el RTL original y la netlist de compuertas sintetizada para probar que son
funcionalmente idénticos bajo todas las entradas posibles. Adicionalmente, se realiza la
Simulación a Nivel de Compuertas (Gate-Level Simulation - GLS). GLS es significativamente
más lenta en ejecución y más compleja de configurar que la simulación RTL, pero es
indispensable para validar el diseño utilizando una representación que incluye detalles del
hardware sintetizado, como la estructura exacta del árbol de reloj, la lógica de reset generada
por las herramientas, y cómo se propagan los estados desconocidos ('X') debido a condiciones
de reset incompletas o contención de señales. La netlist de compuertas es una representación
mucho más voluminosa y menos legible para los humanos que el código RTL, lo que hace que
la depuración de cualquier discrepancia o error descubierto en este nivel sea
considerablemente más difícil y laboriosa, a menudo requiriendo el análisis de miles o millones
de instancias de celdas lógicas.

●Consideraciones post-layout (Timing, Power, Efectos Físicos).
Tras la síntesis, el diseño pasa a la etapa de layout o diseño físico. Aquí, los elementos de la
netlist de compuertas son colocados físicamente en la superficie del chip (place), y sus
interconexiones (cables metálicos) son trazadas para conectarlos según la netlist (route). Esta
etapa final determina la geometría exacta del diseño en el silicio. Como resultado de este
proceso, se puede extraer información detallada y precisa sobre los retrasos temporales de las

compuertas individuales y, crucialmente, los retrasos y efectos parásitos (resistencias,
capacitancias, inductancias) de las interconexiones. La verificación post-layout aborda cómo
estos aspectos físicos impactan la corrección funcional y el rendimiento del diseño. Aunque el
Análisis de Timing Estático (Static Timing Analysis - STA) es la herramienta principal para
verificar que el diseño cumple con todas las restricciones de timing (setup/hold times,
frecuencias máximas) a lo largo de todas las rutas de señal, la verificación funcional a bajo
nivel debe considerar que el comportamiento lógico real ahora ocurre con los retrasos del
mundo real extraídos del layout. La Simulación a Nivel de Compuertas con información de
timing anotada (GLS con SDF - Standard Delay Format) se utiliza para verificar que el diseño
funcionalmente complejo aún se comporta correctamente cuando se operan con estos retrasos
físicos. Esto es especialmente importante para verificar el funcionamiento correcto en la
frecuencia de operación objetivo, validar caminos lógicos sensibles al timing no cubiertos
completamente por STA (como ciertos caminos asíncronos o lógicas de control críticas en
modos de baja potencia), o verificar el impacto de la variabilidad del proceso en la
funcionalidad. Similarmente, se consideran los aspectos de potencia: la distribución física de la
potencia (power grids), las caídas de voltaje (IR drop) debido a la actividad dinámica, y el
consumo de potencia en diferentes modos operativos. La verificación con conciencia de
potencia (Power-Aware Verification - PAV), a menudo utilizando formatos estándar como
UPF/CPF para describir la intención de potencia, y la simulación que considera estos efectos
aseguran el funcionamiento correcto en diferentes estados de potencia y durante las
transiciones, previniendo glitches o fallos funcionales inducidos por problemas de potencia.
Otros efectos físicos, como el acoplamiento entre cables vecinos (crosstalk) que puede inducir
ruido y potencialmente causar que un '0' se lea como un '1' (o viceversa), la integridad de la
señal en buses de alta velocidad, la variabilidad debido a la temperatura o el voltaje (PVT
variations), y las posibles vías de ataque físico o de canal lateral (que dependen directamente
de la estructura física), también entran dentro del espectro de las consideraciones de bajo nivel
que impactan la corrección y la seguridad, y que deben ser verificados o considerados en este
nivel de detalle físico y estructural.

●[Desarrollo del Ejemplo para 1.2]
Consideremos una Máquina de Estados Finitos (FSM) simple que controla el acceso a un
recurso, pasando por estados como IDLE, REQUEST, GRANT y ERROR. La FSM se describe
inicialmente en RTL utilizando SystemVerilog.
Verificación a Nivel RTL: En RTL, verificaríamos esta FSM mediante simulación funcional y
posiblemente verificación formal de propiedades.
●Simulación: Creamos test vectors que aplican secuencias de entrada esperadas (ej.
IDLE -> REQUEST -> GRANT -> IDLE) y secuencias inesperadas (ej. REQUEST ->
REQUEST) para asegurar que la FSM transiciona correctamente entre estados y
produce las salidas de control adecuadas.

●Formal (SVA): Podríamos escribir propiedades SVA para formalizar su comportamiento,
como:
○assert property (@(posedge clk) $rose(grant) |-> ##1
!request);
(Si se otorga el permiso, la petición debe desactivarse en el
siguiente ciclo).
○assert property (@(posedge clk) state == ERROR |-> ##[1:*]
state == IDLE);
(Si la FSM entra en estado de error, eventualmente debe
volver a IDLE).
○assert property (@(posedge clk) state != IDLE |->
$stable(request) or $rose(request) or $fell(request));
(Si no
está en IDLE, la señal de petición debe ser estable o cambiar, es parte de la
lógica que la mantiene fuera de IDLE). La verificación formal en RTL puede
probar que estas propiedades son verdaderas para todos los estados
alcanzables y secuencias de entrada posibles, asegurando la corrección lógica
de la FSM. Verificación a Nivel de Compuertas (Post-Síntesis): Ahora, esta descripción RTL es
sintetizada por una herramienta, que la mapea a una netlist de compuertas utilizando la
biblioteca de tecnología de destino. El código RTL podría ser simple y claro, pero la
herramienta de síntesis podría aplicar optimizaciones que resulten en una netlist con lógica
reestructurada o con caminos que no corresponden uno a uno con el RTL original.
●Equivalence Checking (FEC): El primer paso crítico es ejecutar FEC entre el RTL
original y la netlist de compuertas sintetizada. Esta herramienta formal intenta probar
matemáticamente si la netlist produce exactamente las mismas salidas que el RTL para
todas las posibles combinaciones de entradas en todos los ciclos de reloj. Si hay alguna
diferencia funcional (un bug introducido por la síntesis), FEC lo detectará y
proporcionará un contraejemplo.

●Gate-Level Simulation (GLS): Aunque FEC verifica la equivalencia funcional lógica,
GLS es necesaria para verificar el diseño a nivel de compuertas, especialmente cuando
se añade información de timing. Consideremos un escenario hipotético donde la FSM,
en su implementación RTL, genera una señal de "habilita_escritura" (write_enable) que
se supone que debe activarse en el mismo ciclo que la señal "GRANT". Durante la
síntesis, debido a optimizaciones o a las características específicas de las celdas de la
biblioteca, la ruta lógica que genera "habilita_escritura" podría tener un pequeño retardo
adicional en la netlist de compuertas en comparación con la ruta de "GRANT". Aunque
FEC confirmaría que lógicamente ambas señales se activan en el mismo ciclo en
ausencia de retrasos, una GLS posterior con anotaciones de timing (SDF) podría revelar
que, en la frecuencia de reloj objetivo, "habilita_escritura" llega ligeramente tarde
respecto a "GRANT", violando un requisito de setup en la entrada del recurso al que
controla. Este es un bug funcional dependiente del timing de la implementación física,
introducido por la síntesis y visible solo en la netlist de compuertas con información de
retardo. Este tipo de error sería difícil de detectar solo en RTL o con GLS sin timing

preciso. La GLS post-síntesis (y especialmente post-layout con SDF preciso) es
esencial para identificar estos fallos que surgen de la traducción del RTL a la
implementación física.

Este ejemplo ilustra claramente que la verificación a bajo nivel no se detiene en RTL. Se deben
aplicar técnicas de verificación a nivel de compuertas (FEC para equivalencia lógica, GLS para
comportamiento con estructura sintetizada y timing) para asegurar que las transformaciones del
diseño no introducen errores.

1.3 ¿Por Qué la Verificación Tradicional es Insuficiente?
Históricamente, la verificación de hardware se basaba predominantemente en la simulación
utilizando vectores de prueba dirigidos manualmente. Este enfoque, que consistía en aplicar
secuencias de entrada predefinidas y comparar las salidas del diseño bajo prueba con el
comportamiento esperado, fue adecuado para circuitos de menor complejidad y alcances
funcionales limitados. Sin embargo, con la explosión de la escala y la funcionalidad de los
ASICs y FPGAs modernos, así como la integración de múltiples fuentes de complejidad (IPs,
heterogeneidad), esta estrategia tradicional ha demostrado ser cada vez más ineficaz y costosa
para proporcionar la confianza necesaria en la corrección y, especialmente, en la seguridad del
diseño a bajo nivel. Las limitaciones inherentes de la simulación dirigida la hacen inadecuada
para abordar los desafíos de la complejidad actual, dejando amplias áreas del diseño sin
verificar adecuadamente.
●Limitaciones de la simulación dirigida (Test Vectors
específicos).
La simulación dirigida es un método de verificación en el que los ingenieros crean
manualmente conjuntos específicos de entradas (vectores de prueba) con el fin de ejercitar
funcionalidades particulares del diseño, verificar rutas lógicas conocidas, o validar respuestas a
condiciones de error predefinidas. Por ejemplo, para un controlador de interfaz de red, se
podrían crear vectores para enviar y recibir un paquete de datos correctamente formado, probar
casos de error como paquetes corruptos o desbordamientos de buffer simulados, o verificar la
inicialización y configuración del dispositivo. La debilidad fundamental de este enfoque reside
en su predictibilidad limitada: solo verifica el diseño para los escenarios exactos contemplados
por los vectores de prueba cuidadosamente diseñados. La calidad y la exhaustividad de la
verificación quedan intrínsecamente ligadas a la capacidad del ingeniero para anticipar todos
los comportamientos posibles, incluyendo los casos de esquina (corner cases), las
interacciones inusuales entre módulos y las secuencias de eventos menos obvias. Es un
proceso altamente dependiente de la intuición y la experiencia humana, lo que lo hace
propenso a omitir escenarios no previstos. La simulación dirigida es muy buena para validar
que las funcionalidades conocidas operan como se espera, pero es inherentemente pobre para

encontrar errores o vulnerabilidades no anticipadas o que se manifiestan solo bajo condiciones
muy específicas. Para diseños modernos con un número masivo de modos operativos,
configuraciones posibles y complejas interacciones concurrentes, desarrollar manualmente un
conjunto de vectores de prueba que cubra adecuadamente un porcentaje suficientemente alto
del comportamiento posible se vuelve una tarea prohibitivamente laboriosa, extremadamente
costosa en tiempo y recursos, y, en la práctica, casi imposible de completar de manera
exhaustiva. Se convierte en un esfuerzo desproporcionado con respecto a la cobertura de
verificación que realmente se logra.

●El problema del espacio de estados (State Space Explosion).
La insuficiencia de la simulación dirigida se agrava exponencialmente por el fenómeno
conocido como la "explosión del espacio de estados". El estado de un diseño digital síncrono
en un momento dado está completamente definido por los valores almacenados en todos sus
elementos de memoria (principalmente flip-flops, latches y celdas de memoria). Si un diseño
tiene N elementos de memoria binaria (como flip-flops), el número total de estados posibles que
el diseño puede potencialmente alcanzar es 2N. Para poner esto en perspectiva, un diseño
modesto con solo 100 flip-flops tiene 2100 estados posibles, un número con más de 30 dígitos
(1.26×1030). Un diseño de SoC real puede tener cientos de miles o millones de flip-flops,
resultando en un número de estados más allá de cualquier comprensión humana o capacidad
computacional para enumerar. La simulación, ya sea dirigida o incluso aleatoria simple, solo
"visita" una fracción infinitesimal de este vasto espacio de estados. Aunque se ejecuten miles
de millones o billones de ciclos de reloj simulados, la probabilidad de que estos ciclos, a través
de transiciones secuenciales, ejerciten una secuencia particular de eventos o alcancen un
estado de error específico que reside en un rincón remoto del diseño es increíblemente baja.
Las técnicas de simulación tradicional no tienen una estrategia inherente o eficiente para
"dirigir" la exploración del espacio de estados hacia áreas problemáticas o no visitadas de
manera sistemática. Esto significa que, incluso con extensas granjas de simulación, grandes
porciones del comportamiento potencial del diseño pueden permanecer efectivamente sin
verificar, dejando la puerta abierta a la existencia de fallos latentes que solo se manifestarán
una vez que el chip esté fabricado y operando en un entorno del mundo real. La longitud de las
secuencias de eventos (profundidad secuencial) necesaria para alcanzar ciertos estados o
activar ciertas lógicas también contribuye a este problema, haciendo que la simulación sea muy
ineficiente para hallar bugs que requieren un camino largo y específico en el espacio de
estados.

●La dificultad de identificar errores o vulnerabilidades sutiles y
de rara ocurrencia.
Quizás el mayor peligro de depender únicamente de la verificación tradicional es su debilidad
para descubrir los errores más costosos y las vulnerabilidades de seguridad más insidiosas.
Estos no suelen ser fallos obvios que se manifiestan durante el funcionamiento básico, sino que

son fallos "profundos" o "de rara ocurrencia". A menudo, se manifiestan solo bajo condiciones
muy específicas que involucran interacciones complejas y multifacéticas entre múltiples
bloques del diseño, secuencias de eventos asíncronos inusuales (como la llegada casi
simultánea de múltiples solicitudes concurrentes o interrupciones), estados de configuración de
esquina que rara vez se utilizan, la operación en los límites de las condiciones de voltaje o
temperatura, o el impacto combinado de múltiples factores operacionales junto con valores de
datos particulares. Por ejemplo, un error puede requerir una latencia de comunicación particular
en el bus de interconexión combinada con una carga de procesamiento específica en un core y
un evento externo inusual que active una lógica de manejo de errores. Las vulnerabilidades de
seguridad, como los Hardware Trojans o los puntos débiles explotables por ataques de canal
lateral, están diseñados precisamente para ser sutiles y activarse o revelar información solo
bajo condiciones que un vector de prueba funcional típico probablemente no generaría.
Depender de la simulación de escenarios predefinidos significa que, a menos que el verificador
anticipe precisamente el escenario del fallo raro, nunca se activará. Depender de la simulación
aleatoria simple es como buscar una aguja en un pajar cósmico; aunque teóricamente podría
encontrar el fallo raro, la probabilidad por unidad de tiempo de simulación es tan baja que no es
una estrategia de verificación viable o eficiente. Las metodologías de verificación tradicional, al
carecer de la capacidad de explorar el espacio de estados de manera sistemática, guiada o
exhaustiva (como lo hacen las técnicas formales o la simulación aleatoria restringida
avanzada), son intrínsecamente deficientes para descubrir estos fallos "esquivos" que
constituyen una amenaza significativa y costosa para la corrección y seguridad del diseño una
vez que el chip está en producción.

●[Desarrollo del Ejemplo para 1.3]
Consideremos un diseño de un controlador de interrupciones complejo en un SoC, que
maneja múltiples fuentes de interrupción asíncronas con diferentes prioridades (por ejemplo, de
un controlador de red, un temporizador, un controlador DMA y un periférico externo). El
controlador tiene lógica para arbitrar entre interrupciones concurrentes, enmascarar ciertas
fuentes y señalizar la CPU cuando una interrupción está lista para ser procesada.
Verificación Tradicional (Simulación Dirigida): Un enfoque de verificación tradicional con
simulación dirigida crearía test vectors para:
●Verificar que una única interrupción de alta prioridad se maneja correctamente.
●Verificar que una única interrupción de baja prioridad se maneja correctamente.
●Verificar que el enmascaramiento de interrupciones funciona.
●Verificar que dos interrupciones conocidas con diferentes prioridades se manejan
secuencialmente cuando llegan con una separación temporal clara.
●Verificar que el reset limpia todas las interrupciones pendientes.
Estos test funcionarían y mostrarían que el controlador maneja los casos "obvios" y previstos.

El Fallo Sutil y Raro: Sin embargo, el controlador de interrupciones podría tener un fallo sutil
de diseño que solo se manifiesta bajo una condición de carrera muy específica a bajo nivel:
cuando dos interrupciones de la misma prioridad (o dos prioridades con una lógica de arbitraje
compleja y menos probada) llegan con una diferencia de tiempo mínima, cayendo dentro de
una ventana de metaestabilidad potencial en la lógica de arbitraje interna, o desencadenando
una secuencia inusual de accesos concurrentes a un registro de estado compartido. En este
escenario raro, la lógica de arbitraje podría entrar en un estado incorrecto, resultando en: ●Una de las interrupciones se pierde por completo.
●Ambas interrupciones son reconocidas, pero el controlador señaliza incorrectamente a
la CPU o se corrompe el estado interno del controlador, llevando a un bloqueo (hang) o
un comportamiento impredecible.
●Las prioridades se invierten inesperadamente para esas dos interrupciones
concurrentes específicas.
Por qué la Simulación Tradicional Falla Aquí:
●Simulación Dirigida: Es muy poco probable que un ingeniero de verificación anticipe y
diseñe manualmente un vector de prueba que genere precisamente esa condición de
llegada casi simultánea o esa secuencia exacta de eventos de prioridad idéntica con el
timing crítico. El test solo activará el fallo si la ventana de tiempo crítica se acierta con
precisión, lo cual es una coincidencia rara.
●Simulación Aleatoria Simple: Una simulación aleatoria sin restricciones podría,
teóricamente, generar interrupciones con timing aleatorio. Sin embargo, la probabilidad
de que dos interrupciones específicas lleguen dentro de la estrecha ventana de tiempo
que activa el fallo, en medio de un gran número de ciclos de simulación y otros eventos
aleatorios en el SoC, es extremadamente baja. Sería como esperar ganar una lotería
específica con un número enorme de posibles resultados. Este ejemplo ilustra cómo los fallos de rara ocurrencia, a menudo ligados a condiciones de
carrera o interacciones de timing muy específicas en lógica concurrente a bajo nivel, pasan
desapercibidos en la verificación tradicional. Su descubrimiento requiere metodologías que
puedan explorar el espacio de estados de manera más exhaustiva (Formal) o generar
estímulos de manera más inteligente y dirigida a cubrir interacciones complejas y condiciones
de esquina (Simulación Aleatoria Restringida avanzada con buena cobertura).
1.4 La Convergencia de la Corrección Funcional y la Seguridad
Tradicionalmente, las disciplinas de verificación de la corrección funcional y la seguridad de
hardware se han gestionado con cierta separación, a menudo por equipos diferentes con
conocimientos y herramientas distintos. Los ingenieros de verificación funcional se centraban
en asegurar que el diseño implementara correctamente su especificación de comportamiento
deseado bajo todas las condiciones operativas válidas, mientras que los especialistas en

seguridad se ocupaban de la resistencia a ataques maliciosos externos o internos. Sin
embargo, la realidad de los diseños modernos, la creciente sofisticación de los atacantes y la
naturaleza de las vulnerabilidades a bajo nivel ha puesto de manifiesto una convergencia
fundamental e inseparable entre estos dos ámbitos. Los fallos en la implementación de la
funcionalidad o la seguridad de un diseño pueden ser la causa o la manifestación de problemas
en el otro, haciendo indispensable un enfoque de verificación que considere ambos aspectos
de manera integrada desde las etapas tempranas del diseño hasta la implementación final a
bajo nivel. ●Errores funcionales que pueden ser explotados como
vulnerabilidades de seguridad.
Un error en el diseño de hardware que causa un comportamiento funcional incorrecto, aunque
no haya sido introducido con intención maliciosa, puede crear una debilidad o una puerta
trasera que un atacante astuto puede identificar y explotar con fines maliciosos. Consideremos
un fallo de verificación funcional que se manifiesta como una condición de carrera (race
condition) en la lógica de control de acceso a un recurso compartido, como un registro de
configuración crítico o una región de memoria protegida. Si la lógica de arbitraje entre dos
solicitantes (uno autorizado, uno no autorizado) no se ha verificado rigurosamente para todas
las posibles llegadas de solicitudes, podría existir una ventana temporal muy pequeña en la que
una solicitud no autorizada pueda "ganar" la carrera y obtener acceso momentáneo al recurso
antes de que se apliquen completamente los permisos de seguridad. Este es un fallo funcional
(la lógica de arbitraje no es robusta), pero se convierte en una vulnerabilidad de seguridad
explotable por un atacante que pueda controlar el timing de sus solicitudes. Otro ejemplo podría
ser un error en el manejo de errores o excepciones. Si un diseño no gestiona adecuadamente
un fallo interno o una entrada inválida, podría entrar en un estado de operación no definido
donde, por ejemplo, las señales de control de seguridad por defecto no se aplican, dejando
brevemente expuestos registros internos con información sensible. Un "buffer overflow" de
hardware (análogo al software) en una FIFO o un buffer on-chip, si no se limita correctamente a
bajo nivel, podría permitir que una escritura excesiva sobrescriba registros de control vecinos,
alterando inesperadamente el comportamiento del chip y posiblemente desactivando
mecanismos de seguridad. La clave aquí es que el fallo original es un error funcional, pero su
consecuencia puede ser una brecha de seguridad si un atacante puede activarlo y aprovechar
el comportamiento anómalo. La verificación tradicional, enfocada solo en el comportamiento
funcional "correcto", puede pasar por alto las condiciones que activan estos estados
vulnerables.

●Vulnerabilidades de seguridad que impactan la funcionalidad
(Ej: Hardware Trojans).
La relación también funciona de forma bidireccional: elementos o modificaciones introducidas
en el diseño o en la cadena de suministro con una intención explícitamente maliciosa pueden
alterar directamente el comportamiento funcional del diseño. El ejemplo más prominente y

ampliamente discutido de esto son los Hardware Trojans. Un Troyano es una adición o
modificación sigilosa al circuito que permanece inactivo hasta que se activa por una "condición
de disparo" (trigger) muy específica. Este trigger puede ser lógico (una secuencia de entradas
de control inusual, un estado interno particular), basado en timing (una coincidencia temporal
entre dos eventos inesperada), o incluso ambiental (operación fuera de un rango de
temperatura o voltaje esperado). Una vez activado, el Troyano ejecuta una "carga útil"
(payload) maliciosa que intencionalmente altera la funcionalidad pretendida del chip. Las
cargas útiles pueden variar ampliamente: podrían deshabilitar una función crítica (Denial of
Service), degradar sutilmente el rendimiento de un algoritmo criptográfico, filtrar información
secreta (como claves de cifrado) modificando las salidas de datos, permitir acceso no
autorizado creando una puerta trasera funcional, o causar fallos intermitentes y difíciles de
diagnosticar. A diferencia de los errores funcionales no intencionados, estas modificaciones son
deliberadas, a menudo diseñadas para ser pequeñas, ocultas y activarse solo bajo condiciones
que las técnicas de verificación funcional convencional rara vez ejercitarían. Otro ejemplo
menos dramático podría ser una puerta trasera funcional deliberadamente insertada por un
diseñador deshonesto: una combinación de entradas o un estado que, aunque no forma parte
de la especificación funcional oficial, activa una funcionalidad de depuración secreta o un
acceso privilegiado no documentado. En ambos casos (Troyanos, backdoors maliciosos), la
vulnerabilidad de seguridad se manifiesta como una alteración del comportamiento funcional
del diseño a bajo nivel, requiriendo técnicas de verificación y análisis que buscan
específicamente este tipo de desviaciones o funcionalidades ocultas.

●La necesidad de un enfoque unificado.
La profunda interdependencia entre la corrección funcional y la seguridad a nivel de hardware a
bajo nivel subraya la necesidad crítica de adoptar un enfoque de verificación integrado y
holístico. Ya no es seguro ni eficiente verificar la funcionalidad sin considerar activamente las
posibles implicaciones de seguridad de los errores o las interacciones inesperadas que puedan
surgir en la implementación de bajo nivel, ni verificar la seguridad ignorando cómo las posibles
vulnerabilidades pueden manifestarse como fallos funcionales o degradaciones del
rendimiento. Una estrategia de verificación robusta debe considerar ambos aspectos
simultáneamente, aplicando metodologías y técnicas que puedan abordar la complejidad de
asegurar tanto la corrección como la seguridad. Las metodologías de verificación avanzadas,
tanto las formales como las basadas en simulación inteligente, ofrecen el potencial para
abordar esta convergencia de manera efectiva. Las técnicas formales empleadas para probar la
corrección de propiedades funcionales (Ej: "esta salida siempre refleja la suma de las entradas
después de N ciclos") pueden ser adaptadas y extendidas para demostrar la ausencia de
ciertas clases de vulnerabilidades de seguridad (Ej: probando propiedades de aislamiento -
"esta región de memoria protegida nunca es accesible desde este puerto externo", o
propiedades de no interferencia/flujo de información seguro - "los datos clasificados como
'secreto' nunca fluyen hacia un puerto de salida clasificado como 'público'"). Las sofisticadas
estrategias de generación de estímulos y análisis de cobertura de la verificación basada en
simulación avanzada (CRV/CDV en entornos como UVM) pueden utilizarse para dirigir la

verificación no solo hacia casos de esquina funcionales difíciles, sino también para generar
secuencias de eventos que podrían actuar como triggers para Hardware Trojans o revelar
debilidades de canal lateral que se manifiestan en el comportamiento funcional o temporal.
Presentar un panorama completo y riguroso de la garantía de calidad de hardware a bajo nivel
requiere, por tanto, abordar la corrección y la seguridad no como objetivos separados, sino
como facetas interconectadas del mismo desafío fundamental: asegurar que el silicio se
comporta exacta y únicamente como se pretendía, sin fallos explotables ni funcionalidades
ocultas maliciosas, a pesar de la creciente complejidad y las potenciales amenazas en la
cadena de suministro.

●[Desarrollo del Ejemplo para 1.4]
Consideremos un sistema simplificado donde un registro interno sensible (por ejemplo, que
contiene una clave criptográfica) debe ser accesible únicamente cuando el chip opera en un
modo "seguro", indicado por una señal de control
secure_mode activa (secure_mode = 1).
La lógica a bajo nivel (a nivel de compuertas o post-layout) que controla la lectura de este
registro incluye una compuerta lógica (por ejemplo, una AND) que habilita la salida del registro
solo si
secure_mode es alta.
Verilog
// Representación conceptual a bajo nivel
always @(*) begin
if (secure_mode) begin
sensitive_reg_output = sensitive_key_register;
end else begin
sensitive_reg_output = 'z; // Alta impedancia o valor fijo no sensible
end
end

(En una implementación real, esto sería lógica a nivel de compuertas controlando buffers o
multiplexores).
El Fallo Funcional (Glitch de Timing): Supongamos que, debido a un error de diseño a bajo
nivel o a variabilidad en el proceso de fabricación, la señal de control
secure_mode tiene una
ruta lógica que, bajo una condición de operación específica y rara (por ejemplo, una
combinación particular de actividad en bloques vecinos y una transición de voltaje), se retrasa
mínimamente al pasar de alto a bajo. En otras palabras, hay un "glitch de timing": secure_mode debería volverse baja y deshabilitar la salida del registro simultáneamente con
otro evento de control, pero se retrasa una pequeña fracción de nanosegundo más de lo
esperado.

La Vulnerabilidad de Seguridad Explotable: Este pequeño fallo de timing funcional crea una
"ventana de exposición". Si un atacante conoce el diseño (quizás por ingeniería inversa) y
puede controlar o sincronizar sus acciones con la transición de
secure_mode, podría intentar
leer la salida de
sensitive_reg_output precisamente durante esa diminuta ventana de
tiempo extra. Durante esa fracción de nanosegundo, la compuerta de control aún podría estar
habilitando la salida del registro sensible porque
secure_mode aún no ha caído
completamente, mientras que la lógica de control en el dominio no seguro ya podría estar lista
para capturar el valor de
sensitive_reg_output.
Por qué esto es una Convergencia y Requiere Verificación Unificada:
●Origen Funcional: El problema inicial es un fallo funcional de timing a bajo nivel: una
señal de control no cumple su requisito de tiempo en un escenario específico.
●Consecuencia de Seguridad: Este fallo funcional abre una brecha de seguridad crítica
al exponer información confidencial.
●Requerimiento de Verificación Unificada: La verificación funcional tradicional
(simulación RTL sin timing preciso) probablemente no detectaría este glitch de timing
dependiente de la implementación física. El Análisis de Timing Estático (STA) podría
identificar la ruta lenta de
secure_mode, pero a menos que se definan restricciones de
seguridad explícitas relacionadas con esta señal, STA solo lo marcaría como una
violación de timing si afecta un path de timing funcional estándar (setup/hold), no
necesariamente como una brecha de seguridad. Detectar esta vulnerabilidad requiere: ○Verificación a bajo nivel con timing: Ejecutar Gate-Level Simulation con
anotaciones SDF precisas post-layout que capturen el retardo real de
secure_mode, o
○Verificación Formal de Seguridad: Especificar formalmente que "si
secure_mode es bajo, entonces sensitive_reg_output nunca debe reflejar
el valor de
sensitive_key_register". Una herramienta formal podría
entonces buscar un contraejemplo (una secuencia de eventos o un estado
donde esta propiedad se viola), posiblemente identificando la rara condición que
causa el glitch de timing o un estado donde la lógica de habilitación falla
independientemente del timing.
Este ejemplo ilustra perfectamente cómo un problema que nace de la implementación física y el
timing a bajo nivel (un error funcional) puede convertirse en una vulnerabilidad de seguridad
crítica. Destaca la necesidad de que los procesos de verificación de corrección funcional y
seguridad se integren, utilizando técnicas como GLS con timing y Verificación Formal para
analizar el diseño en un nivel de detalle donde estos fallos sutiles se manifiestan.

Capítulo 2: Fundamentos de la Verificación de
Hardware y los Desafíos del Bajo Nivel
Antes de adentrarnos en las metodologías avanzadas de Verificación Formal y de Diseño, es
fundamental establecer una base sólida sobre el proceso general de diseño de hardware y los
tipos de errores comunes que surgen, prestando especial atención a los desafíos particulares
que se presentan en los niveles de abstracción más bajos, es decir, el RTL y el nivel de
compuertas. Este capítulo presenta una visión general del flujo típico de desarrollo de ASICs y
FPGAs, clasifica los tipos de fallos a considerar y ahonda en las complejidades específicas
asociadas con la verificación en estas etapas críticas cercanas a la implementación física.

2.1 El Proceso de Diseño y Verificación de ASICs/FPGAs
El desarrollo de un circuito integrado moderno es un proceso complejo y multifacético que
involucra una secuencia de etapas interconectadas, a menudo referidas como el "flujo de
diseño". La verificación no es una etapa lineal al final de este proceso, sino una disciplina
paralela y omnipresente que se integra en casi todas las fases, desde la concepción hasta la

fabricación. La comprensión de este flujo es esencial para posicionar correctamente las
diferentes técnicas de verificación y apreciar por qué la detección temprana de errores es tan
crucial.

●El Proceso de Diseño y Verificación de ASICs/FPGAs.
El flujo típico de diseño digital comienza con la Especificación, un documento detallado que
describe el comportamiento funcional deseado, los requisitos de rendimiento, las restricciones
de potencia, el tamaño y las interfaces del circuito. A partir de la especificación, se define la
Arquitectura, que es una descripción de alto nivel de la estructura del sistema, dividiéndolo en
bloques principales y definiendo cómo interactúan. Luego viene la etapa de Diseño RTL,
donde se implementa la arquitectura utilizando un lenguaje de descripción de hardware (HDL)
como Verilog o SystemVerilog, describiendo el comportamiento en términos de transferencia de
datos entre registros. Es en este punto donde el diseño funcional se codifica por primera vez.
Paralelamente al diseño RTL, se lleva a cabo la Verificación RTL, que constituye la parte más
extensa y compleja de la verificación funcional. Una vez que el diseño RTL se considera
funcionalmente correcto, pasa a la Síntesis Lógica, donde las herramientas automatizadas
traducen la descripción RTL a una Netlist de Compuertas utilizando una biblioteca de
tecnología de fabricación específica. Después de la síntesis, se realiza la Verificación
Post-Síntesis, que incluye la verificación de equivalencia formal para asegurar que la netlist de
compuertas es lógicamente equivalente al RTL. La siguiente etapa es el Diseño Físico (Place
& Route), donde las celdas lógicas de la netlist de compuertas se colocan físicamente en el
plano del chip y se trazan las interconexiones metálicas. Este proceso es seguido por la
Verificación Post-Layout, que extrae información precisa de timing (parásitos de
interconexión) y realiza análisis estáticos y dinámicos (como GLS con SDF) para confirmar que
el diseño físico cumple con todos los requisitos temporales, de potencia y de integridad de
señal. Finalmente, para ASICs, se procede a la Fabricación del silicio, mientras que para
FPGAs, la netlist final se utiliza para Programar el dispositivo. La verificación, en sus diversas
formas (simulación, formal, estática), se integra en múltiples puntos de este flujo.

●Posicionamiento de las diferentes etapas de verificación.
La verificación no es una actividad que espera hasta que el diseño esté "terminado". Es un
proceso iterativo que comienza tan pronto como las primeras partes del diseño RTL están
disponibles. La verificación a nivel de bloque se realiza primero, seguida de la verificación a
nivel de subsistema y finalmente a nivel de chip completo (SoC). Las metodologías de
verificación funcional (principalmente simulación RTL) se aplican intensivamente durante la fase
de diseño RTL. La Verificación Formal, como el Equivalence Checking y el Model Checking, se
utiliza también en paralelo o después de la síntesis y para verificar propiedades específicas a lo
largo del flujo. Las verificaciones que dependen de la implementación física, como GLS con
timing, análisis de timing estático (STA) y verificación de potencia (PAV), se realizan después de
la síntesis y, crucialmente, después del layout, cuando la información física está disponible.
Existe una tendencia fuerte hacia el "shift-left" en la verificación, es decir, intentar verificar lo
máximo posible en las etapas más tempranas del diseño (arquitectura, RTL) para evitar que los
errores se propaguen a fases posteriores, donde son mucho más costosos de corregir.
●El costo de los errores en etapas tardías (Respines).
El costo de encontrar y corregir un error de diseño aumenta exponencialmente a medida que el
diseño avanza en el flujo. Un error descubierto y corregido durante la codificación RTL es
relativamente barato, requiriendo solo cambios en el código y re-verificación. Sin embargo, si el
mismo error se descubre después de la síntesis, requiere modificar el RTL, re-verificar RTL,
re-sintetizar, y re-verificar la netlist de compuertas. Si se descubre después del layout, implica
modificar el RTL, re-verificar, re-sintetizar, re-hacer el layout y re-verificar post-layout. Para un
ASIC, un error funcional descubierto después de la fabricación (en el silicio) es el escenario
más costoso y desastroso, a menudo requiriendo un "respin" completo del chip. Un respin
implica generar un nuevo conjunto de fotomáscaras (extremadamente caras, pueden costar
millones de dólares en nodos avanzados), fabricar una nueva tanda de chips, y repetir todas las
etapas de prueba, lo que se traduce en meses de retraso y una pérdida financiera
considerable. Incluso para FPGAs, un error funcional descubierto después de que el diseño
está implementado en hardware puede requerir meses de depuración y un rediseño sustancial.
Un consenso común en la industria es que el costo de corregir un bug se multiplica por un
factor de 10x o más por cada etapa principal que se avanza en el flujo de diseño (RTL ->
Síntesis -> Layout -> Silicio). Esta realidad económica y temporal subraya por qué es
imperativo invertir en metodologías de verificación robustas y exhaustivas en las etapas de bajo
nivel.

●[Desarrollo del Ejemplo para 2.1]
Ilustremos el flujo de diseño y verificación de un ASIC con un diagrama de flujo simplificado y
consideremos el impacto de encontrar un bug en diferentes etapas.
Fragmento de código

graph TD
A[Especificación] --> B(Arquitectura);
B --> C{Diseño RTL};
C --> D{Verificación RTL};
D -- Bugs encontrados --> C;
D -- Diseño Verificado --> E[Síntesis Lógica];
E --> F{Verificación Post-Síntesis<br>(FEC, GLS sin timing)};
F -- Bugs encontrados --> C;
F -- Diseño Verificado --> G[Diseño Físico<br>(Place & Route)];
G --> H{Verificación Post-Layout<br>(STA, GLS con SDF, PAV)};
H -- Timing/Funcional Bugs --> C;
H -- Layout Correcto --> I[Fabricación];
I --> J[Pruebas Post-Fabricación];
J -- Bugs encontrados --> C;
J -- Chips Funcionales --> K[Producto Final];

%% Style for nodes
style C fill:#f9f,stroke:#333,stroke-width:2px
style D fill:#ccf,stroke:#333,stroke-width:2px
style E fill:#fcf,stroke:#333,stroke-width:2px
style F fill:#ccf,stroke:#333,stroke-width:2px
style G fill:#f9f,stroke:#333,stroke-width:2px
style H fill:#ccf,stroke:#333,stroke-width:2px
style I fill:#fcf,stroke:#333,stroke-width:2px
style J fill:#ccf,stroke:#333,stroke-width:2px

%% Verification paths
D -- Métodos Formales (Model Checking) --> C;
H -- Métodos Formales (Timing Properties) --> C;
Consideremos el Costo de un Bug:
1.Bug encontrado durante Verificación RTL (D): Un bug funcional menor se detecta
durante la simulación RTL. La corrección implica modificar unas pocas líneas en el
código RTL (C). Luego, solo es necesario re-simular la parte afectada o ejecutar una
regresión RTL (D). Costo: Bajo. Horas o días de trabajo del ingeniero. 2.Bug encontrado durante Verificación Post-Síntesis (F): Un bug sutil, quizás
relacionado con la lógica de reset generada por la herramienta de síntesis, se detecta
durante GLS post-síntesis. La corrección implica modificar el RTL (C), re-simular RTL
(D), re-sintetizar el diseño (E), y luego re-verificar post-síntesis (F). Costo: Medio. Días
o semanas de trabajo, dependiendo del tamaño del diseño y el tiempo de síntesis.
3.Bug encontrado durante Verificación Post-Layout (H): Un bug funcional sensible al
timing, por ejemplo, una condición de carrera que solo se manifiesta con los retrasos
reales de las interconexiones, se detecta durante GLS con SDF. La corrección implica
modificar el RTL (C), re-simular RTL (D), re-sintetizar (E), re-hacer el diseño físico

(Place & Route) (G), y finalmente re-verificar post-layout (H). Re-hacer el layout es un
proceso que consume mucho tiempo computacional y humano. Costo: Alto. Semanas
o meses de trabajo, uso intensivo de recursos computacionales.
4.Bug encontrado durante Pruebas Post-Fabricación (J): Un error funcional o de
timing muy raro que solo se manifiesta a temperaturas extremas se descubre en los
chips fabricados. Este es el peor escenario. La corrección implica identificar el bug en el
RTL (C) (lo cual puede ser muy difícil en silicio), re-verificar todo el flujo (D, E, F, G, H), y
lo más costoso: generar nuevas fotomáscaras y fabricar una nueva tanda de chips (I).
Costo: Muy Alto. Millones de dólares y meses de retraso en el lanzamiento del
producto ("Respin"). Este diagrama y la consideración del costo ilustran poderosamente por qué la verificación
exhaustiva a bajo nivel, desde RTL hasta post-layout, es una inversión crítica para evitar los
desastrosos costos de encontrar errores en etapas tardías del ciclo de desarrollo de hardware.
Las metodologías avanzadas buscan precisamente reducir drásticamente la probabilidad de
que estos errores se propaguen aguas abajo.

2.2 Tipos de Errores de Diseño Comunes
El objetivo primordial de la verificación es descubrir errores o "bugs" en el diseño antes de que
el hardware sea fabricado o desplegado. Estos errores pueden manifestarse de diversas
formas, afectando no solo el comportamiento funcional deseado, sino también características
no funcionales críticas como el timing, el consumo de potencia y, como hemos visto, la
seguridad. Clasificar los tipos de errores ayuda a entender la variedad de problemas que las
técnicas de verificación a bajo nivel deben ser capaces de identificar.
●Errores funcionales (Lógica incorrecta).
Los errores funcionales constituyen la categoría más amplia y a menudo la primera que se
busca en la verificación. Se refieren a cualquier desviación del comportamiento especificado, es
decir, el diseño no realiza la operación lógica o el control de la manera esperada. Estos errores
pueden originarse en una variedad de fuentes durante la codificación RTL o incluso en etapas
de abstracción superior. Incluyen:
○Errores de lógica combinacional: Expresiones booleanas incorrectas, tablas
de verdad incompletas, o fallos en la implementación de la lógica de decisión.
○Errores en Máquinas de Estados Finitos (FSMs): Transiciones de estado
incorrectas o faltantes bajo ciertas entradas, estados inalcanzables, deadlocks
(la FSM se queda atrapada en un ciclo del que no puede salir) o livelocks (la
FSM circula continuamente entre un conjunto de estados sin progresar hacia el
estado deseado), o la FSM entra en estados no definidos/ilegales.

○Errores en rutas de datos (Datapaths): Lógica aritmética o lógica incorrecta
(por ejemplo, un sumador que resta, un comparador que funciona al revés),
desbordamiento (overflow) o subdesbordamiento (underflow) no manejado
correctamente, o errores en la manipulación de bits. ○Errores en lógica de control: Secuencia incorrecta de operaciones, fallos en la
lógica de arbitraje para recursos compartidos, o problemas en el manejo de
condiciones de excepción o error.
○Errores de protocolo: Violaciones de las reglas de timing, secuencia o formato
de datos de una interfaz de comunicación (por ejemplo, una señal de
handshaking que se activa en el momento incorrecto). Estos errores son el
objetivo principal de la verificación RTL y la simulación funcional exhaustiva. ●Violaciones de timing (Setup/Hold violations, Clock Domain
Crossing - CDC).
Los errores de timing ocurren cuando las señales de datos no llegan a los elementos de
memoria (como flip-flops) dentro de las ventanas de tiempo requeridas relativas al borde del
reloj. El timing es especialmente crítico en diseños síncronos de alta velocidad. Las dos
violaciones de timing más comunes son:

○Setup Violation: La señal de datos cambia demasiado tarde y no se estabiliza
antes del borde activo del reloj en la entrada de un flip-flop. El flip-flop puede
capturar un valor metaestable o incorrecto.
○Hold Violation: La señal de datos cambia demasiado pronto después del borde
activo del reloj, no manteniéndose estable durante el tiempo requerido. Esto
puede causar que el flip-flop capture el nuevo valor prematuramente. Estas
violaciones se analizan principalmente mediante Análisis de Timing Estático
(STA) post-layout, pero los errores funcionales relacionados con timing pueden
requerir verificación dinámica (GLS con SDF) o formal para ser completamente
comprendidos y depurados. Un subtipo crítico de error de timing funcional ocurre
en los límites de Clock Domain Crossing (CDC). Cuando las señales se
transfieren entre partes del diseño que operan con relojes diferentes y
asíncronos, existe el riesgo de metaestabilidad si las señales no se sincronizan
correctamente. Un fallo en la lógica de sincronización CDC puede llevar a la
propagación de valores indeterminados ('X' en simulación), la pérdida o
duplicación de pulsos de control, o la incoherencia de datos en buses. La
verificación formal es a menudo indispensable para garantizar la corrección de la
lógica CDC.
●Problemas de potencia (Glitches, IR drop, Power sequencing).
Con el enfoque en la eficiencia energética, los diseños modernos implementan esquemas
complejos de gestión de potencia, como múltiples dominios de voltaje, apagado de dominios de
potencia (power gating) y escalado dinámico de voltaje y frecuencia (DVFS). La verificación
debe asegurar que el diseño funcione correctamente en todos los modos de potencia y durante

las transiciones entre ellos. Los problemas comunes incluyen:

○Glitches: Picos transitorios de voltaje inesperados en señales que deberían ser
estables, a menudo causados por transiciones de potencia, cambios de voltaje o
actividad en dominios vecinos. Un glitch en una señal de control crítica puede
activar lógica secuencial inesperadamente, llevando a un error funcional. ○IR Drop: Caída de voltaje en la red de distribución de potencia debido a la
resistencia de las interconexiones y la alta demanda de corriente durante picos
de actividad. Un IR drop excesivo puede reducir el voltaje de alimentación local
en algunas celdas, ralentizando su operación y potencialmente causando
violaciones de timing funcionalmente relevantes que no se detectan con un
análisis de timing basado en voltaje nominal.
○Power Sequencing: El orden correcto y el timing de activación/desactivación de
diferentes dominios de potencia y señales de reset son cruciales. Un error en la
secuencia puede dejar partes del diseño en un estado desconocido, causar
contención en buses o dañar el hardware. La verificación debe asegurar que la
lógica de control de potencia (power management unit) opera según lo
especificado.
●Vulnerabilidades de seguridad (Hardware Trojans, Backdoors, Side
Channels).
Como se presentó en el Capítulo 1, los errores que comprometen la seguridad son una clase
creciente de "bugs" que requieren una verificación específica. Estos no siempre se manifiestan
como fallos funcionales obvios en operación normal.

○Hardware Trojans: Circuitos maliciosos insertados subrepticiamente que se
activan bajo condiciones específicas y ejecutan una carga útil dañina, alterando
la funcionalidad, filtrando información o negando servicio.
○Backdoors: Caminos de acceso intencionalmente diseñados y no
documentados que permiten bypassar los controles de seguridad estándar para
obtener acceso privilegiado.
○Vulnerabilidades de Canal Lateral: Debilidades en la implementación que
permiten a un atacante extraer información secreta (como claves criptográficas)
analizando características físicas como el consumo de potencia, el tiempo de
ejecución de operaciones o las emisiones electromagnéticas. ○Ataques de Fault Injection: Susceptibilidad a la manipulación externa (por
ejemplo, picos de voltaje, láser) que puede inducir fallos temporales o
permanentes explotables. La verificación de seguridad a bajo nivel busca
identificar la susceptibilidad del diseño a estos tipos de ataques, a menudo
requiriendo técnicas que analizan la implementación física y lógica de manera
diferente a la verificación funcional tradicional.

[Desarrollo del Ejemplo para 2.2]
Para ilustrar la variedad de errores, consideremos un módulo simplificado de procesamiento
de paquetes en un chip de red:
1.Error Funcional (en FSM): El módulo incluye una FSM para parsear la cabecera de los
paquetes entrantes. Un error de codificación en RTL hace que la FSM, al recibir un
paquete con una longitud de cabecera específica inusual (pero válida según el
protocolo), omita uno de los estados de parsing. Esto resulta en que ciertos campos de
la cabecera no se lean correctamente y los datos subsiguientes se interpreten mal.

○Impacto: Fallo de procesamiento funcional para un tipo específico de paquete.
Detectable en simulación RTL con un test vector específico para ese paquete.
2.Violación de Timing (Setup): Una señal de control generada por la lógica de parsing
de la FSM (que es crítica para la lógica de la ruta de datos) debe llegar a un flip-flop de
registro de datos antes del borde de reloj para cumplir su tiempo de setup. Sin embargo,
después del layout, la ruta física de esta señal es más larga de lo esperado, y su retardo
real (capturado en el SDF) causa una violación de setup en la frecuencia de operación
máxima del chip.

○Impacto: Fallo funcional intermitente en operación a alta velocidad o bajo ciertas
condiciones PVT, donde el flip-flop puede capturar datos incorrectos. STA
debería detectarlo, pero GLS con SDF puede confirmarlo y ayudar en la
depuración, especialmente si el fallo depende de un patrón de datos o actividad
específico.
3.Problema de Potencia (Glitch por Power Gating): El módulo de procesamiento de
paquetes está en un dominio de potencia que puede ser apagado cuando está inactivo.
La lógica de control de power gating (implementada parcialmente con lógica de
compuertas) tiene un error: durante el encendido de este dominio, se genera un glitch
transitorio en la señal de reset local que se propaga brevemente a otros dominios. Este
glitch activa inesperadamente la lógica de inicialización de otro módulo dependiente,
poniéndolo en un estado incorrecto antes de que el reset principal del sistema se
desactive.

○Impacto: Fallo funcional del sistema al salir de un modo de bajo consumo.
Detectable con simulación power-aware (utilizando UPF/CPF) que modela las
transiciones de voltaje y las señales de control de power gating.
4.Vulnerabilidad de Seguridad (Hardware Trojan): Un pequeño Hardware Trojan se
inserta subrepticiamente en la lógica de padding del paquete. Este Trojan tiene un
trigger basado en timing muy sutil: se activa solo si se recibe un paquete de un tamaño
específico (ej. 128 bytes) y el controlador de interrupciones (en otro módulo) genera una
interrupción en el mismo ciclo de reloj. Cuando se activa, el payload del Troyano altera
sutilmente la cabecera del paquete saliente para desviar el tráfico a una dirección IP

maliciosa.

○Impacto: Riesgo de seguridad; el chip puede ser cooptado para redirigir tráfico.
Este fallo es difícil de detectar porque combina una condición funcional
específica (tamaño del paquete) con una condición de timing/evento rara
(interrupción concurrente específica) en otro módulo, diseñada para eludir la
verificación funcional estándar. Requiere análisis de seguridad especializado y
técnicas de verificación avanzadas para buscar triggers y payloads ocultos. Este ejemplo demuestra que los errores pueden ocurrir en diferentes "dimensiones"
(funcionalidad, timing, potencia, seguridad) y a diferentes niveles de bajo nivel (RTL,
compuertas, post-layout), y a menudo requieren técnicas de verificación distintas para su
identificación.

2.3 Desafíos Específicos de la Verificación a Nivel RTL
El nivel de transferencia de registros (RTL) es, como se presentó, el punto donde la mayoría de
la lógica funcional se concreta y, por lo tanto, donde se introduce la mayoría de los errores
funcionales. La verificación en RTL es la base de la garantía de corrección funcional. Sin
embargo, las características propias de la descripción RTL de hardware complejo presentan
desafíos particulares que van más allá de la simple ejecución de código. A diferencia del
software secuencial, el hardware es inherentemente concurrente y opera bajo restricciones
temporales y de recursos que deben ser cuidadosamente consideradas. ●Manejo de la concurrencia.
El hardware digital opera en paralelo. En una descripción RTL, múltiples bloques de código
(
always blocks, assign statements concurrentes en Verilog/SystemVerilog) se ejecutan
conceptualmente de forma simultánea o en respuesta a eventos de reloj o cambios de señal.
La verificación RTL debe asegurar que la interacción entre estas unidades concurrentes es
correcta bajo todas las posibles alineaciones temporales y órdenes de llegada de eventos. Esto
incluye:
○Arbitraje de recursos compartidos: Cuando múltiples módulos intentan
acceder al mismo recurso (por ejemplo, un puerto de memoria, un bus), la lógica
de arbitraje debe garantizar que solo uno accede a la vez y que se evitan
condiciones de inanición (starvation). ○Sincronización: Asegurar que las operaciones que dependen de eventos que
ocurren en diferentes partes del diseño (o en respuesta a entradas asíncronas)
se sincronizan correctamente para evitar condiciones de carrera o pérdida de
datos.

○Comunicación entre procesos: Validar que la comunicación entre módulos
concurrentes (por ejemplo, utilizando handshaking signals, FIFOs) se adhiere a
los protocolos definidos y no introduce interbloqueos (deadlocks). Depurar
problemas de concurrencia en simulación RTL puede ser difícil porque el
resultado exacto de una condición de carrera puede depender de las
peculiaridades del simulador o del timing exacto de los eventos, que puede
variar ligeramente entre ejecuciones o herramientas. Comprender y verificar
rigurosamente las interacciones concurrentes es un desafío central en RTL.
●Verificación de Interfaces y Protocolos complejos.
Los diseños modernos de SoC están compuestos por múltiples bloques que se comunican a
través de interfaces bien definidas. Estas interfaces a menudo implementan protocolos
complejos, ya sean estándares de la industria (como AXI, AHB, PCIe, USB, Ethernet) o
protocolos internos personalizados. Estos protocolos especifican secuencias precisas de
handshaking, formatos de datos, reglas de timing entre señales y respuestas esperadas a
transacciones válidas e inválidas. La verificación en RTL debe asegurar que cada módulo se
adhiere estrictamente a la especificación de la interfaz que implementa o a la que se conecta.
Esto implica generar una amplia gama de transacciones válidas e inválidas en la interfaz
(simulación), verificar que el módulo responde correctamente (ej. aceptando datos, señalizando
ocupado, generando errores), y, para protocolos complejos, a menudo requiere el uso de
"modelos de referencia" o "scoreboards" que actúan como implementaciones ideales del
protocolo para comparar el comportamiento del diseño bajo prueba. La complejidad de estos
protocolos aumenta la dificultad de la verificación RTL, haciendo que la creación manual de test
dirigidos sea ineficiente para cubrir todos los posibles escenarios de protocolo, incluyendo
casos de esquina y manejo de errores.

●Asegurar la resetabilidad correcta.
El mecanismo de reset (reinicialización) es fundamental en hardware para poner el diseño en
un estado inicial conocido y seguro al encender o en respuesta a un evento externo. Una lógica
de reset defectuosa puede impedir que el chip se inicialice correctamente, causando fallos
desde el principio de la operación. La verificación en RTL debe asegurar que todos los
elementos de estado (flip-flops, registros de memoria) se inicializan correctamente a sus
valores predeterminados después de un reset, independientemente de su estado inicial. Si el
reset es asíncrono (independiente del reloj), su manejo en los límites de los dominios de reloj
presenta desafíos CDC adicionales, ya que una señal de reset asíncrona que libera cerca del
borde de reloj puede causar metaestabilidad. La verificación debe confirmar que la lógica de
sincronización de reset asíncrono es robusta. Para diseños complejos con múltiples dominios
de potencia y reloj, la secuencia de aplicación y liberación de los resets puede ser intrincada y
dependiente de la unidad de gestión de potencia; verificar esta secuencia correcta a bajo nivel
(RTL) es vital. Además, en simulación, los elementos no reinicializados correctamente o con
lógica de inicialización ambigua pueden adoptar un estado desconocido ('X'), y verificar cómo
este estado 'X' se propaga a través de la lógica (X-propagation) es crucial para no enmascarar

fallos funcionales. Un diseño correctamente reinicializado debería salir de un estado 'X' a un
estado conocido después del reset.

[Desarrollo del Ejemplo para 2.3]
Consideremos un buffer FIFO (First-In, First-Out) asíncrono descrito en RTL. Un FIFO es
una estructura de datos que permite que datos escritos en un dominio de reloj (
wr_clk) sean
leídos en otro dominio de reloj diferente (
rd_clk), manejando automáticamente las diferencias
de frecuencia y fase entre los relojes. La verificación a nivel RTL de un FIFO asíncrono
presenta los desafíos de concurrencia e interacción entre dominios.
Diseño RTL Simplificado del FIFO:
●Dos punteros (read pointer rd_ptr y write pointer wr_ptr) que siguen la posición de
los datos en la memoria interna.
●Lógica para incrementar wr_ptr con wr_clk cuando se escribe un dato.
●Lógica para incrementar rd_ptr con rd_clk cuando se lee un dato.
●Lógica para generar señales de full (FIFO lleno) y empty (FIFO vacío) comparando
wr_ptr y rd_ptr. Esta lógica debe funcionar correctamente incluso si los punteros
cambian de forma asíncrona entre sí.
●Una pequeña memoria interna para almacenar los datos.
Desafíos de Verificación RTL a Bajo Nivel y Cómo el Ejemplo los Ilustra:
1.Manejo de la Concurrencia: La lógica de escritura y la lógica de lectura operan
concurrentemente e independientemente una de la otra, activadas por sus respectivos
relojes. La verificación debe asegurar que no haya condiciones de carrera cuando
ambos dominios intentan acceder o actualizar el estado interno (como los punteros o las
señales
full/empty) casi simultáneamente. ¿Qué pasa si se intenta leer y escribir
exactamente al mismo tiempo? ¿Se corrompen los punteros? ¿Se pierde un dato? Esto
es un problema de concurrencia pura en RTL.
2.Verificación de Interfaces y Protocolos (Implícito): El FIFO tiene una interfaz de
escritura (data in, write enable, full out) y una interfaz de lectura (data out, read enable,
empty out). Verificar el FIFO implica asegurar que respeta su protocolo interno: no
permitir escrituras cuando está lleno, no permitir lecturas cuando está vacío, y garantizar
que la señal
full se activa solo cuando la memoria está realmente llena y empty solo
cuando está realmente vacía.

3.Sincronización y CDC (Crucial para FIFO Asíncrono): El desafío más crítico es la
sincronización de los punteros entre los dominios de reloj. El dominio de escritura

necesita "ver" el rd_ptr (que opera con rd_clk) para saber si el FIFO está lleno. De
manera similar, el dominio de lectura necesita "ver" el
wr_ptr (que opera con wr_clk)
para saber si el FIFO está vacío. Debido a que los relojes son asíncronos, los punteros
(o versiones sincronizadas de ellos) deben cruzar el límite del dominio de reloj utilizando
sincronizadores CDC (generalmente flip-flops en cascada). Un error en el diseño o la
verificación de estos sincronizadores CDC a bajo nivel (RTL) puede llevar a:

○Metaestabilidad: Si un puntero cambia justo cuando el flip-flop del sincronizador
lo muestrea en el otro dominio, el flip-flop puede entrar en un estado
metaestable, propagando un valor indeterminado que podría causar que la lógica
full/empty se active o desactive incorrectamente.
○Incoherencia de Punteros: Si los punteros no se sincronizan correctamente, el
dominio de escritura podría pensar que el FIFO aún tiene espacio cuando en
realidad está lleno (causando sobreescritura y corrupción), o el dominio de
lectura podría pensar que hay datos disponibles cuando no los hay (causando
lectura de basura o subdesbordamiento). A menudo se usan punteros
Grey-coded para minimizar los errores de sincronización, pero la lógica de
comparación de punteros cruzados y los sincronizadores siempre necesitan
verificación rigurosa.
Cómo la Verificación RTL Aborda Esto:
●Simulación RTL: Se usan testbenches con generadores de estímulos que pueden
operar en diferentes dominios de reloj, aplicando escrituras y lecturas
concurrentemente, con diferentes velocidades de reloj, deteniendo y reiniciando relojes,
y aplicando reset. Se usan scoreboards para verificar que los datos escritos son
idénticos a los datos leídos y que no hay pérdida o corrupción. Se modela y verifica la
lógica
full/empty. Sin embargo, probar todas las alineaciones temporales críticas
entre eventos asíncronos en simulación es extremadamente difícil.
●Verificación Formal: Para la lógica de sincronización CDC de los punteros y la lógica
full/empty, la verificación formal (Model Checking) es invaluable. Se pueden escribir
propiedades formales para probar, por ejemplo:
○assert property (@(posedge wr_clk) full |-> !wr_en); (No se
permite escribir cuando está lleno).
○assert property (@(posedge rd_clk) empty |-> !rd_en); (No se
permite leer cuando está vacío).
○Propiedades más complejas sobre la relación entre los punteros sincronizados
cruzados y el estado real del FIFO para probar la corrección de la lógica
full/empty bajo cualquier condición de timing asíncrono de los punteros de
origen.
○Análisis formal específico de la lógica CDC para garantizar la robustez de los
sincronizadores y la ausencia de metaestabilidad que pueda afectar la lógica
funcional aguas abajo.

Este ejemplo de FIFO asíncrono ilustra a fondo cómo la verificación a nivel RTL debe lidiar con
la complejidad de la concurrencia, la interacción entre dominios de reloj asíncronos y la
garantía de que el diseño funcional (en este caso, el bufferado confiable de datos) se comporta
correctamente a pesar de estas complejidades inherentes del hardware a bajo nivel.

2.4 Desafíos Específicos de la Verificación a Nivel de
Compuertas (Gate-Level)
La verificación a nivel de compuertas (Gate-Level Verification) aborda el diseño después de que
ha sido transformado por la herramienta de síntesis en una red de elementos lógicos y
secuenciales de una biblioteca tecnológica específica. Si bien el RTL es el nivel principal para
la verificación funcional, el nivel de compuertas presenta un conjunto distinto de desafíos que
requieren atención específica, ya que las características de implementación física comienzan a
influir en el comportamiento lógico. Asegurar la corrección y fiabilidad en este nivel es un paso

crítico antes de pasar al diseño físico.

●Impacto de la síntesis y optimizaciones.
El proceso de síntesis lógica es una transformación compleja y, a menudo, agresiva. Las
herramientas de síntesis toman la descripción RTL y, basándose en restricciones de diseño
(velocidad, área, potencia), la traducen a una netlist de compuertas optimizada. Esto implica
seleccionar celdas de la biblioteca, mapear lógica combinacional a estas celdas y reestructurar
la lógica (por ejemplo, compartiendo subexpresiones lógicas o factorizando lógica) para cumplir
con las restricciones. Si bien generalmente las herramientas de síntesis son muy confiables, no
son infalibles. Un error en la herramienta, un comando de restricción incorrecto o una
peculiaridad en la forma en que se mapea el RTL a la biblioteca pueden resultar en una netlist
de compuertas que no es funcionalmente idéntica al RTL original. Peor aún, las optimizaciones

pueden, de forma inadvertida, exponer bugs latentes en el RTL que antes estaban
enmascarados (por ejemplo, una condición de carrera o una lógica combinacional no deseada
que la estructura RTL original impedía que se activara). La verificación a nivel de compuertas
debe detectar estas discrepancias introducidas por el proceso de síntesis, que son difíciles de
depurar una vez que se manifiestan en la netlist.

●Verificación con Información de Timing e Interconexiones (SDF).
En el nivel RTL, la simulación funcional generalmente considera que la lógica combinacional no
tiene retardo (delayless) o utiliza modelos de retardo simplificados. Sin embargo, en el nivel de
compuertas, y más precisamente después del layout, los retrasos reales de las celdas lógicas y,
de manera crucial, los retrasos parásitos introducidos por las interconexiones (cables metálicos
en el chip) se vuelven significativos. Estos retrasos dependen del tamaño de las celdas, la
carga capacitiva que deben impulsar, y la longitud y resistencia de los cables. El formato SDF
(Standard Delay Format) es el estándar de la industria para representar estos retrasos
extraídos después del layout. La Simulación a Nivel de Compuertas con anotaciones SDF (GLS
con SDF) es esencial para verificar el comportamiento funcional del diseño operando con estos
retrasos reales. STA (Análisis de Timing Estático) es la herramienta principal para verificar que
no hay violaciones de setup/hold en las rutas síncronas, pero STA es "estático" y no verifica el
comportamiento dinámico o secuencial del diseño con timing real. GLS con SDF puede revelar
fallos funcionales que dependen de la interacción de la lógica con los retrasos reales, como:

○Pulsos de control que se vuelven demasiado estrechos o demasiado anchos
debido a la propagación a través de la lógica con retrasos específicos, activando
erróneamente lógica secuencial aguas abajo.
○Condiciones de carrera funcionales que solo se manifiestan cuando los retrasos
en diferentes caminos lógicos se alinean de una manera particular
post-síntesis/layout.
○Comportamiento inesperado en lógica asíncrona o lógica de reset sensible al
timing fino que no se capturó completamente en STA.
●Manejo de Señales Tri-estado y X-propagation.
En el diseño de hardware, a menudo es necesario que múltiples módulos puedan "conducir"
una misma señal física (por ejemplo, en un bus interno). Esto se logra utilizando drivers
tri-estado, que pueden estar en estado alto ('1'), bajo ('0') o alta impedancia ('Z', efectivamente
desconectado). La verificación a nivel de compuertas debe asegurar rigurosamente que en
cualquier momento, solo un driver está activo (no en 'Z') en una señal dada. Si dos drivers
intentan conducir la misma señal a valores opuestos ('0' y '1') simultáneamente (contención),
esto puede llevar a resultados impredecibles o incluso dañar físicamente el chip. GLS se utiliza
para verificar que la lógica de control que habilita los drivers tri-estado previene la contención
en todos los escenarios operativos. Relacionado con esto está el manejo de X-propagation.
En simulación, un estado desconocido o indeterminado se representa con 'X'. Los estados 'X'

pueden surgir de flip-flops no reinicializados, contención en buses, o entradas no especificadas.
Verificar a nivel de compuertas implica asegurar que los 'X' no se propaguen de manera que
enmascaren bugs funcionales (por ejemplo, si una señal de control se vuelve 'X' pero una
compuerta OR aguas abajo trata 'X' como '0', permitiendo que la lógica proceda
incorrectamente). Una simulación de compuertas robusta debe verificar que la lógica del diseño
se comporta predeciblemente incluso en presencia de 'X's temporales o que la lógica de reset o
inicialización limpia correctamente los 'X's.
●Consideración de Efectos Físicos a nivel de Compuertas
(revisitando).
Aunque muchos efectos físicos se analizan completamente solo después del layout, algunos
comienzan a ser relevantes para la verificación funcional y de timing ya en el nivel de
compuertas cuando se añade información de retardo. El IR drop, por ejemplo, puede modelarse
de forma simplificada post-síntesis e impactar los retardos de las celdas, lo cual es visible en
GLS con SDF. El crosstalk entre interconexiones vecinas, aunque su análisis detallado es
post-layout, puede, en casos extremos, causar que un pulso de ruido en una señal 'víctima' sea
lo suficientemente grande como para ser muestreado por un flip-flop aguas abajo, un fallo
funcional activado por un fenómeno físico que puede manifestarse en una GLS con modelos
parásitos básicos o avanzados. La verificación a nivel de compuertas es el primer punto donde
el comportamiento funcional del diseño comienza a ser evaluado con una representación que
considera la implementación lógica y los primeros impactos de la física.

[Desarrollo del Ejemplo para 2.4]
Para ilustrar los desafíos a nivel de compuertas y la necesidad de GLS con timing,
consideremos un simple datapath con un multiplexor (MUX) controlado por una señal de
selección asíncrona (o una señal síncrona con una ruta de control muy larga) en un diseño
que también tiene lógica de control para ese MUX.
Diseño (Conceptual RTL):
Verilog
// RTL conceptual
reg data_out;
wire select_mux; // Señal de control del MUX

always @(*) begin
if (select_mux) begin
data_out = data_input_b;
end else begin

data_out = data_input_a;
end
end

// select_mux se genera a partir de lógica de control compleja...
// ... que podría tener una ruta larga o depender de lógica asíncrona.
assign select_mux = complex_control_logic_output;

En RTL y simulación funcional simple, asumimos que select_mux cambia y el data_out del
MUX cambia "instantáneamente" después.
Después de la Síntesis (Netlist de Compuertas):
La herramienta de síntesis implementa el MUX usando compuertas lógicas y la
complex_control_logic como una red de compuertas. La señal select_mux ahora tiene
una ruta física real con un retardo no trivial desde el flip-flop que genera
complex_control_logic_output hasta el pin de selección del MUX implementado con
compuertas.
El Fallo Potencial a Nivel de Compuertas y la Verificación con Timing (GLS con SDF):
Supongamos que hay un escenario de operación raro (quizás activado por una secuencia de
control particular o una interrupción asíncrona) donde la señal
select_mux cambia casi al
mismo tiempo que la señal
data_input_b cambia, pero con un retardo ligeramente mayor de
lo esperado debido a la ruta física de
select_mux en la netlist sintetizada (y anotado en el
SDF post-layout). En este escenario, el MUX, implementado con compuertas, podría capturar
un valor de
data_input_b viejo o transitorio en lugar del nuevo valor correcto, antes de que la
señal
select_mux se estabilice en su nuevo estado. Esto es una condición de carrera
funcional activada por los retrasos reales en la lógica de control a nivel de compuertas.
●STA: Si la ruta de select_mux no es una ruta de timing síncrona estándar (setup/hold)
con respecto a un flip-flop aguas abajo que registre
data_out, o si la verificación STA
no incluyó una restricción de "false path" o "multi-cycle path" correcta para esta lógica
de control específica, STA podría no marcar esta ruta como problemática.
●GLS con SDF: Ejecutar una Simulación a Nivel de Compuertas con los retrasos reales
extraídos post-layout (SDF) para este escenario específico revelaría que el valor de
data_out no es el esperado en el ciclo de reloj subsiguiente. Se vería cómo la señal
select_mux tarda en cambiar y cómo, durante ese breve período, el MUX selecciona
data_input_b con un valor incorrecto debido al retardo de select_mux relativo al
cambio de
data_input_b. La depuración de esto implicaría examinar las trazas de
señal a nivel de compuertas con los retardos SDF para identificar la condición de
carrera exacta.

Este ejemplo ilustra cómo la verificación a nivel de compuertas, especialmente cuando se
consideran los retardos de implementación física (GLS con SDF), es fundamental para
identificar fallos funcionales que surgen de la traducción del RTL a la netlist real y de la
interacción de la lógica con los tiempos de propagación reales de las señales a bajo nivel.
Estos fallos no serían visibles en la simulación RTL idealizada.

Capítulo 3: Verificación Formal: Probanza
Matemática de la Corrección
Mientras que la verificación basada en simulación valida el comportamiento de un diseño
mediante la ejecución de escenarios específicos, la Verificación Formal (FV) ofrece un enfoque
radicalmente diferente: utiliza métodos matemáticos rigurosos para probar o refutar la
corrección de un diseño con respecto a una especificación formalizada (un conjunto de
propiedades). En el contexto de la verificación a bajo nivel de hardware, la FV se ha convertido
en una herramienta indispensable, capaz de identificar clases de errores y vulnerabilidades que
son prácticamente imposibles de encontrar solo con simulación, proporcionando un nivel de
garantía de corrección que va más allá de la simple validación. Este capítulo se adentra en los
fundamentos, técnicas y aplicaciones de la Verificación Formal en el dominio de ASICs y
FPGAs, mostrando cómo permite un aseguramiento más profundo de la funcionalidad y la
seguridad a nivel de implementación.

3.1 Introducción a la Verificación Formal
La Verificación Formal representa un paradigma distinto en el aseguramiento de la calidad del
hardware. En lugar de ejecutar el diseño con entradas de prueba y observar las salidas, la FV
opera sobre una representación matemática del diseño y un conjunto de propiedades
expresadas en un lenguaje formal. El objetivo es utilizar algoritmos para probar lógicamente si
el diseño siempre satisface (o nunca viola) esas propiedades, cubriendo sistemáticamente
todos los posibles escenarios dentro del alcance de la propiedad.
●¿Qué es la Verificación Formal?
En esencia, la Verificación Formal es el proceso de utilizar técnicas matemáticas para verificar
la corrección de un sistema (en nuestro caso, un diseño de hardware digital) con respecto a
una especificación formal. No se trata de ejecutar el diseño en el tiempo (como en la
simulación), sino de analizarlo lógica y matemáticamente para determinar si cumple ciertas
propiedades. El diseño bajo verificación se modela utilizando un formalismo matemático
adecuado para representar su comportamiento lógico y secuencial, a menudo un sistema de
transición de estados o un conjunto de fórmulas lógicas (Ver Apéndice: Símbolos y
Notaciones Utilizadas). Las propiedades que se desean verificar (por ejemplo, "la salida X
nunca es alta si la entrada Y es baja", "la respuesta siempre llega entre 3 y 5 ciclos después de
la petición") se expresan en un lenguaje de especificación de propiedades formal con sintaxis y
semántica precisas. Las herramientas de FV emplean algoritmos sofisticados para explorar el
espacio de comportamiento posible del modelo del diseño y determinar si las propiedades se
cumplen en todos los estados alcanzables y transiciones lógicas posibles. El resultado de una
verificación formal puede ser una "prueba" (la propiedad es siempre verdadera bajo las
suposiciones del modelo y entorno) o un "contraejemplo" (una secuencia específica de
entradas y estados, comenzando desde un estado inicial, que demuestra una violación de la
propiedad, es decir, ha identificado un bug). Este enfoque ofrece un nivel de rigor que la
simulación, al basarse en un conjunto limitado de ejecuciones finitas, no puede proporcionar,
especialmente para escenarios raros o profundos.

●Contraste con la verificación basada en simulación (Validación
por ejemplos).
La diferencia fundamental entre la Verificación Formal y la verificación basada en simulación
(como la simulación RTL funcional o GLS) radica en su enfoque subyacente y el nivel de
garantía que proporcionan. La simulación es un método empírico o basado en muestreo: valida
el diseño ejecutándolo con un conjunto finito de estímulos de entrada (test vectors, generados
manualmente o aleatoriamente). Solo puede demostrar la presencia de errores (si un test
vector particular los activa), pero no puede demostrar su ausencia. Una simulación exhaustiva
requeriría probar todas las posibles secuencias de entradas para todos los estados
alcanzables, lo cual es computacionalmente inviable para la inmensa mayoría de los diseños
reales debido a la explosión del espacio de estados. La simulación se limita a "validar por

ejemplos": si el diseño funciona correctamente para los miles o millones de casos probados, se
espera que funcione para otros casos, pero no hay una garantía formal. Por el contrario, la
Verificación Formal, cuando es aplicable y escalable para una propiedad dada, puede
proporcionar una "prueba matemática" de corrección o incorrección. Si una propiedad se
prueba formalmente como verdadera, significa que se cumple en todos los estados alcanzables
del diseño que son relevantes para esa propiedad, bajo las suposiciones declaradas sobre el
entorno. Esto ofrece un nivel de confianza mucho mayor sobre la ausencia de ciertos tipos de
bugs dentro del alcance de la propiedad, superando la limitación de la simulación para cubrir
casos raros o no anticipados que no fueron activados por los test. Si encuentra un error, el
contraejemplo formal es determinístico y reproducible, facilitando la depuración.

●Ventajas: Cobertura completa del espacio de estados (en
algunos casos), hallazgo de bugs profundos.
La principal y más poderosa ventaja de la Verificación Formal es su capacidad, para ciertas
clases de problemas y diseños de tamaño manejable formalmente, de analizar
sistemáticamente el espacio de estados relevantes para una propiedad, buscando
exhaustivamente violaciones. Esto contrasta agudamente con la naturaleza de muestreo de la
simulación. Para aspectos críticos de la lógica de control, máquinas de estados finitos (FSMs),
protocolos de interfaz o propiedades de seguridad específicas, la FV puede explorar todos los
caminos lógicos y todas las combinaciones de estados que podrían potencialmente violar una
propiedad, garantizando que si existe un contraejemplo (un bug que viola esa propiedad), la
herramienta lo encontrará (sujeto a limitaciones de escalabilidad y completitud de la propiedad).
Esto hace que la FV sea excepcionalmente buena para descubrir bugs "profundos" o "de rara
ocurrencia" que requerirían secuencias de eventos extremadamente largas o específicas para
ser activados en simulación, o que simplemente no fueron considerados por los ingenieros de
verificación al escribir test dirigidos. La capacidad de obtener una "prueba" formal sobre la
ausencia de una condición de error o sobre la garantía de un comportamiento deseado bajo
suposiciones dadas es una garantía poderosa que la simulación, por su naturaleza empírica, no
puede ofrecer.

●Limitaciones: Escalabilidad, requerimiento de conocimiento
experto, aplicabilidad.
A pesar de sus poderosas capacidades, la Verificación Formal no es una panacea universal y
presenta sus propias limitaciones significativas que deben ser consideradas para su aplicación
efectiva. El desafío más fundamental es la escalabilidad. Aunque los algoritmos formales han
avanzado enormemente (especialmente en el manejo de la explosión del espacio de estados
mediante representaciones simbólicas o basadas en SAT), el problema de verificar propiedades
arbitrarias en diseños funcionales completos de muy gran tamaño sigue siendo una barrera.
Las herramientas pueden tener dificultades para manejar la complejidad de grandes rutas de
datos con lógica aritmética compleja o sistemas de control con un número masivo de flip-flops

secuenciales interdependientes. La aplicación efectiva y eficiente de la FV a menudo requiere
un conocimiento experto considerable por parte del ingeniero de verificación. Se necesita
experiencia tanto en la metodología formal (cómo funcionan las herramientas, qué significan los
resultados, cómo manejar la escalabilidad) como en el diseño bajo verificación para escribir
propiedades significativas que realmente capturen los requisitos importantes y para definir
suposiciones correctas sobre el entorno. Escribir propiedades precisas y completas en un
lenguaje formal es una tarea compleja en sí misma. Finalmente, la FV no es universalmente
aplicable para abordar todos los aspectos de la verificación de hardware que necesita un chip
moderno. Es excelente para verificar la corrección lógica y de control, propiedades de
protocolo, aspectos de conectividad o propiedades de seguridad que pueden formalizarse. Sin
embargo, es menos adecuada o directamente inaplicable (o ineficiente comparada con
simulación) para verificar aspectos como el rendimiento global del sistema (throughput, latencia
bajo carga real), el consumo de potencia dinámico o estático, la funcionalidad de bloques
puramente analógicos o de señal mixta compleja (a menos que se usen modelos abstractos
digitales o técnicas híbridas), o la verificación de software ejecutándose en el hardware. Por lo
tanto, la FV no reemplaza la simulación; la complementa, abordando de manera exhaustiva y
concluyente problemas específicos para los que es particularmente eficaz, mientras que la
simulación se encarga de la validación a nivel de sistema, rendimiento y escenarios del mundo
real.

●[Desarrollo del Ejemplo para 3.1]
Para ilustrar el concepto de Verificación Formal y contrastarla claramente con la simulación
dirigida, consideremos dos ejemplos sencillos que demuestran la diferencia fundamental en el
enfoque y el nivel de garantía obtenido.
Ejemplo 1: Una Compuerta OR de Tres Entradas
●Diseño: Una compuerta lógica OR simple con tres entradas, a, b, y c, y una salida, y,
donde
y = a OR b OR c.

●Objetivo de Verificación: Asegurar que la salida y es alta si, y solo si, al menos una de
las entradas (
a, b, o c) es alta.

●Verificación con Simulación Dirigida: Para una compuerta con 3 entradas, hay 23=8
posibles combinaciones de entradas. Un enfoque de simulación dirigida crearía vectores
de prueba para estas 8 combinaciones. La simulación de estos 8 casos, que
representan todas las combinaciones de entradas posibles para esta compuerta
combinacional, sugiere fuertemente que la compuerta OR funciona correctamente para
todas las entradas válidas. Hemos validado el diseño cubriendo todos los ejemplos

posibles en este caso simple.

●Verificación Formal: Se formaliza el comportamiento deseado como una propiedad
lógica. Por ejemplo, en un lenguaje de propiedades: "La salida
y es verdadera si y solo
si la entrada
a es verdadera, o la entrada b es verdadera, o la entrada c es verdadera".
Matemáticamente: y↔(a∨b∨c) (Ver Apéndice: Símbolos y Notaciones Utilizadas para
↔ y ∨). Una herramienta de Verificación Formal (en este caso, una herramienta de
verificación de equivalencia combinacional o un Model Checker para lógica
combinacional) tomaría la descripción de la compuerta OR de 3 entradas y esta
propiedad formal. Analizaría lógicamente todas las combinaciones de entradas posibles
para verificar la propiedad. A diferencia de la simulación, no "ejecuta" cada caso; utiliza
algoritmos lógicos (basados en BDDs o SAT) para probar si la función booleana
implementada por la compuerta es equivalente a la función booleana definida por la
propiedad. La herramienta probaría que para cada combinación posible de
a, b y c, la
salida
y calculada por la implementación de la compuerta es idéntica al valor esperado
por la propiedad. Dado que la lógica combinacional no tiene estado interno, esta prueba
considera todo el espacio de entradas posibles. El resultado sería que la propiedad es
formalmente probada como verdadera. Esto es una prueba matemática concluyente
de la corrección funcional de la compuerta OR para todas las entradas posibles, no solo
una validación de 8 ejemplos.
Ejemplo 2: Un Contador Sencillo con Lógica de Overflow
●Diseño: Un contador de 4 bits (count[3:0]) que se incrementa en cada ciclo de reloj
cuando una señal
enable es alta. El contador se resetea a 0 cuando una señal
reset_n (activo bajo) es baja. Una señal de salida overflow se activa en el ciclo en
que el contador pasa de 15 a 0.

●Objetivo de Verificación: Asegurar que la señal overflow se activa precisamente
cuando el contador transiciona de su valor máximo (15, binario 1111) a 0.

●Verificación con Simulación Dirigida: Se diseñarían test vectors para simular el
comportamiento del contador bajo diversas condiciones (contando hasta 16,
interrupciones de
enable, reset). Estos test verificarían el comportamiento observado
para las secuencias probadas. Sin embargo, no pueden garantizar que siempre que el
contador llegue a 15 y
enable esté activo, overflow se activará, ni que overflow
nunca se activará en cualquier otro momento. Es difícil de anticipar y probar con
simulación dirigida todos los posibles escenarios de interacción entre
enable y
reset_n en cada estado de la cuenta.

●Verificación Formal (Model Checking): Se formaliza la propiedad deseada. En SVA:
assert property (@(posedge clk) $rose(count == 4'b0000) and

$past(count == 4'b1111, 1) |-> ##0 overflow); (Ver Apéndice: Símbolos y
Notaciones Utilizadas para
@, $rose, ==, and, $past, |->, ##0). Esto afirma que si el
contador sube a 0 y en el ciclo anterior estaba en 15, entonces
overflow debe ser alto
en el mismo ciclo. Y una propiedad de seguridad:
assert property (@(posedge
clk) overflow |-> $past(count == 4'b1111 && enable, 1));
Esto afirma
que si
overflow es alto, entonces en el ciclo anterior el contador debía estar en 15 y
enable debía ser alto. Una herramienta de Model Checking tomaría el modelo formal
del contador (con 4 flip-flops, tiene 24=16 estados alcanzables con
enable y reset_n)
y las propiedades. La herramienta exploraría sistemáticamente todas las secuencias
posibles de entradas
enable y reset_n desde el estado de reset (contador en 0).
Analizaría si existe alguna secuencia que lleve a un estado donde la señal
overflow
se active, pero la condición de transición de 15 a 0 con
enable activo en el ciclo
anterior no se haya cumplido.

○Si la lógica de overflow es correcta, la herramienta Model Checker probará que
las propiedades son siempre verdaderas.
○Si hay un fallo (por ejemplo, la lógica de overflow se activa incorrectamente
cuando el contador transiciona de 7 a 8 debido a un error lógico), la herramienta
encontrará un contraejemplo. La herramienta mostraría la secuencia exacta de
valores de
enable y reset_n que, partiendo de reset, lleva al contador a 7,
luego se activa
enable y, al pasar a 8, la señal overflow se activa
incorrectamente, violando la propiedad.
Estos ejemplos, aunque simples, destacan la diferencia crucial: la simulación valida con
ejemplos específicos; la Verificación Formal, cuando es aplicable y escalable, prueba
matemáticamente la corrección o encuentra contraejemplos para todas las posibilidades dentro
del alcance de la propiedad y el modelo, proporcionando un nivel de garantía superior y siendo
mucho más eficaz para encontrar errores de rara ocurrencia.

3.2 Conceptos Clave de la Verificación Formal
Adentrándose en la práctica de la Verificación Formal, es esencial comprender los conceptos
fundamentales que subyacen a su operación y aplicación. Estos conceptos incluyen cómo se
representa el diseño para el análisis formal, qué tipo de afirmaciones precisas se hacen sobre
él y cómo las herramientas exploran su comportamiento para validar o refutar dichas
afirmaciones. Dominar esta terminología y sus implicaciones es el primer paso para utilizar la
FV de manera efectiva y comprender los resultados de las herramientas. Para la notación
utilizada en fórmulas y propiedades, referirse al Apéndice: Símbolos y Notaciones Utilizadas.

●Modelos formales del diseño.
A diferencia de los simuladores que operan interpretando código HDL o netlists, las
herramientas de Verificación Formal trabajan internamente con una representación
matemática abstracta del diseño bajo verificación, conocida como el "modelo formal". Este
modelo captura la lógica y el comportamiento secuencial del diseño de una manera que es
amenable al análisis algorítmico y matemático. La naturaleza exacta de este modelo puede
variar dependiendo de la técnica de FV y la herramienta utilizada. Para las técnicas de Model
Checking, a menudo se representa el diseño como un sistema de transición de estados o
una red de autómatas finitos, donde cada estado corresponde a una posible configuración de
los elementos de memoria del diseño (los valores de todos los flip-flops, latches y celdas de
memoria en un ciclo dado), y las transiciones entre estados están definidas por la lógica
combinacional y las entradas. Para técnicas como la Verificación de Equivalencia Formal (FEC)
o ciertos tipos de análisis de propiedades estáticas, partes del diseño pueden ser
representadas utilizando estructuras de datos lógicas compactas y eficientes como
Diagramas de Decisión Binarios (BDDs) o mediante conjuntos de fórmulas lógicas
proposicionales o de primer orden que se entregan a solucionadores SAT (Satisfiability) o
SMT (Satisfiability Modulo Theories). La herramienta de FV extrae o construye este modelo
formal a partir de la descripción RTL o la netlist de compuertas del diseño. La precisión y el
nivel de detalle de este modelo formal son cruciales; un modelo que no capture fielmente el
comportamiento del diseño real a bajo nivel puede llevar a pruebas formales incorrectas o

irrelevantes.

●Propiedades a verificar (Assertions, Assumptions, Cover
Properties).
El corazón de la Verificación Formal reside en las propiedades. Las propiedades son las
afirmaciones o requisitos sobre el comportamiento que el diseño debe cumplir (o no cumplir). A
diferencia de un test vector que especifica entradas y salidas esperadas para un momento o
secuencia finita, una propiedad formal especifica el comportamiento de manera universal sobre
todos los estados alcanzables relevantes. Las propiedades se expresan en un lenguaje formal
con sintaxis y semántica bien definidas, como SVA o PSL (presentados en la Sección 3.3). Son
la especificación formal que la herramienta de FV intentará probar con respecto al modelo del
diseño. Existen varios tipos principales de propiedades:

○Assertions (Afirmaciones): Son declaraciones sobre lo que el diseño siempre
debe hacer o lo que nunca debe ocurrir bajo ciertas condiciones. Son la forma
más común de especificar el comportamiento de corrección funcional o
seguridad que se desea probar. Las assertions pueden ser sobre la validez de
una señal en un ciclo específico (ej.
assert signal_x == 1), sobre
relaciones temporales (
assert property (request |-> ##[1:5]
grant);
- si hay una petición, entonces la concesión debe ser verdadera entre
1 y 5 ciclos después), o sobre la exclusión de estados o transiciones indeseadas
(
assert property !(state == IDLE && busy); - el diseño nunca debe
estar inactivo Y ocupado simultáneamente). Si la herramienta de FV encuentra
una secuencia de entradas y estados que hace que una assertion sea falsa, ha
encontrado un bug y lo presenta como un "contraejemplo". ○Assumptions (Suposiciones): Son declaraciones sobre el comportamiento del
entorno del diseño bajo verificación (las señales de entrada) o sobre partes del
diseño que no se están verificando formalmente en ese momento. Las
assumptions restringen el espacio de entradas válidas o el comportamiento de
las señales externas a lo que se espera que ocurra en el sistema real. Por
ejemplo, para verificar un módulo esclavo en un bus, se podría asumir que el
maestro del bus siempre genera transacciones que cumplen estrictamente el
protocolo del bus. Las assumptions son cruciales para limitar el espacio de
estados que la herramienta de FV debe explorar, haciendo que el análisis sea
manejable y centrándolo en escenarios realistas. Sin embargo, es vital que las
assumptions sean precisas y realistas; si una assumption es incorrecta (no se
cumple en el sistema real), la prueba formal de cualquier assertion que dependa
de ella carece de validez.
○Cover Properties (Propiedades de Cubrimiento): A diferencia de las
assertions que buscan violaciones (eventos malos), las cover properties se
utilizan para demostrar la alcanzabilidad de ciertos estados, transiciones o

secuencias de eventos específicos dentro del diseño bajo las assumptions
dadas. Se utilizan para verificar si un escenario particular (por ejemplo, "el
diseño alcanza un estado donde el buffer de entrada está casi lleno") puede
ocurrir. Si la herramienta de FV encuentra una secuencia que hace que una
cover property sea verdadera, ha "cubierto" ese escenario y proporciona la
secuencia. Esto es útil para validar si el modelo formal y las assumptions son lo
suficientemente permisivos para alcanzar escenarios interesantes, y también
puede usarse para medir la "cobertura" formal de ciertos aspectos del
comportamiento del diseño. Si una cover property no puede ser cubierta, puede
indicar un problema en las assumptions (demasiado restrictivas) o en el propio
diseño (el escenario no es realmente alcanzable).
●El concepto de "espacio de estados" y "alcanzabilidad".
Como se mencionó en el Capítulo 1, el espacio de estados de un diseño digital síncrono es el
conjunto de todas las posibles combinaciones de valores que pueden tomar sus elementos de
memoria (flip-flops, etc.). Si un diseño tiene N elementos de memoria binaria, el espacio total
de estados es 2N. En la verificación formal, las herramientas operan sobre el espacio de
estados alcanzables del diseño, que es el subconjunto del espacio total de estados al que el
diseño puede llegar a partir de un estado inicial (generalmente el estado de reset) mediante la
aplicación de secuencias válidas de entradas (consistentes con las assumptions). El objetivo
principal del Model Checking es determinar si existe una ruta (una secuencia de transiciones de
estado) desde el estado inicial de reset a un estado que viola una assertion (o que satisface
una cover property). La "explosión del espacio de estados" sigue siendo el desafío central;
aunque los algoritmos formales utilizan técnicas inteligentes para representar y explorar este
espacio simbólicamente (Ver Apéndice: Símbolos y Notaciones Utilizadas para
representaciones como BDDs) en lugar de enumerar explícitamente cada estado, para diseños
muy complejos, el espacio alcanzable puede ser tan vasto que sobrepasa la capacidad de las
herramientas.

●Invariantes.
Un invariante es un tipo especial y fundamental de assertion. Es una propiedad que debe ser
verdadera en todo estado alcanzable del diseño, sin importar la secuencia de entradas que
llevó a ese estado. Los invariantes a menudo capturan propiedades fundamentales y de alto
nivel sobre la estructura o el comportamiento del diseño que deben mantenerse siempre. Por
ejemplo, un invariante para una cola (queue) bien diseñada podría ser "el número de elementos
válidos en la cola nunca es negativo" o "el puntero de escritura nunca excede al puntero de
lectura en más que la capacidad de la cola". Probar invariantes formalmente puede ser muy
potente, ya que establecer que una propiedad es un invariante proporciona una garantía fuerte
sobre su corrección global. Si se logra probar un invariante, cualquier otra propiedad que se
derive lógicamente de ese invariante también es cierta por extensión.

[Desarrollo del Ejemplo para 3.2]
Veamos ejemplos concretos (utilizando una sintaxis conceptual cercana a SVA) de los
diferentes tipos de propiedades para un módulo de control de lectura desde una memoria
esclava que interactúa con un bus, con señales como
read_req (petición de lectura al
esclavo),
read_grant (esclavo concede la lectura), read_address (dirección a leer),
read_data_valid (datos de lectura válidos disponibles desde el esclavo), y read_data (los
datos leídos). Se asume un reloj
posedge clk. Para la sintaxis SVA, referirse al Apéndice:
Símbolos y Notaciones Utilizadas.
1.Assertion (Afirmación sobre comportamiento deseado): Queremos afirmar que, si el
módulo genera una petición de lectura (
read_req) y el esclavo la concede
(
read_grant), entonces los datos de lectura válidos (read_data_valid) deben estar
disponibles en el bus en algún momento dentro de un rango de ciclos razonable.

○Ejemplo: assert property (@(posedge clk) read_req &&
read_grant |-> ##[3:10] read_data_valid);
■Significado: Si en un ciclo de reloj, tanto read_req como read_grant
son altos, entonces la señal
read_data_valid debe ser alta en algún
momento entre 3 y 10 ciclos de reloj posteriores.
■Propósito: Asegurar que el módulo esclavo al que se conecta el diseño
bajo prueba responde a las peticiones de lectura concedidas dentro de
un límite temporal esperado, verificando así que el diseño espera
correctamente la respuesta. Si la herramienta FV encuentra un
contraejemplo, muestra una secuencia donde
read_req y read_grant
son altos, pero
read_data_valid nunca se activa en los siguientes 10
ciclos, señalando un posible problema en la lógica que espera los datos o
un supuesto incorrecto sobre el esclavo.
2.Assumption (Suposición sobre el entorno/esclavo): Para poder probar la assertion
anterior, debemos asumir que el esclavo realmente concede la petición si es válida, y
que proporciona datos válidos si la petición fue concedida. Estas assumptions
restringen el comportamiento que la herramienta FV modelará para las entradas.
○Ejemplo 1: assume property (@(posedge clk) read_req |->
##[1:2] read_grant);
■Significado: Si la señal read_req es alta en un ciclo, asumimos que la
señal
read_grant proveniente del esclavo se volverá alta entre 1 y 2
ciclos después (el esclavo concede rápidamente).
■Propósito: Restringir el entorno de verificación formal a un
comportamiento realista (y deseado) del esclavo de memoria. Sin esta

assumption, la herramienta FV podría simular escenarios donde el
esclavo nunca concede la petición, y la assertion sobre la respuesta de
datos nunca se activaría, dando una prueba trivial sin valor. Es crucial
verificar también que esta assumption se cumple en el diseño del esclavo
real. ○Ejemplo 2: assume property (@(posedge clk) read_grant |->
##[2:9] read_data_valid);
■Significado: Si la señal read_grant es alta en un ciclo, asumimos que
la señal
read_data_valid proveniente del esclavo se volverá alta
entre 2 y 9 ciclos después (el esclavo proporciona los datos después de
conceder).
■Propósito: Esta assumption, combinada con la anterior y la lógica del
diseño bajo prueba que genera
read_req, es necesaria para que la
assertion sobre
read_data_valid tenga sentido y sea verificable en el
entorno formal.
3.Cover Property (Propiedad de Cubrimiento): Queremos verificar si la herramienta FV
puede alcanzar un escenario donde se realiza una petición de lectura a una dirección
específica (
read_address == 32'h1000) y se reciben los datos correspondientes
(
read_data_valid alto). Esto valida que el flujo de lectura básico es alcanzable en el
entorno formal bajo las assumptions dadas.

○Ejemplo: cover property (@(posedge clk) read_req &&
read_address == 32'h1000 |=> ##[1:*] read_data_valid);
■Significado: Si se emite una petición de lectura para la dirección 0x1000,
buscar una secuencia donde
read_data_valid eventualmente se
vuelva alto.
■Propósito: Confirmar que el modelo formal del diseño y las assumptions
sobre el esclavo y el entorno son lo suficientemente permisivos para
permitir que se complete un ciclo de lectura básico a una dirección
específica. Si esta propiedad no se cubre, podría indicar que una
assumption es demasiado restrictiva o que hay un problema fundamental
que impide la operación de lectura.
4.Invariant (Invariante): Consideremos que el módulo tiene un registro interno
(
state_reg) que rastrea si actualmente está esperando datos de una operación de
lectura (
state_reg == WAITING_FOR_DATA). Queremos asegurar que este estado
solo es activo si se ha emitido una petición (
read_req) y aún no se ha recibido el
read_data_valid correspondiente.

○Ejemplo (simplificado): assert property (@(posedge clk) state_reg
== WAITING_FOR_DATA |-> $past(read_req, [1:15]) &&
!read_data_valid);

■Significado: Siempre que el registro de estado state_reg esté en
WAITING_FOR_DATA, entonces
read_req debía haber estado alto en
alguno de los últimos 1 a 15 ciclos, Y
read_data_valid debe estar
bajo en el ciclo actual. (Este invariante es más complejo de escribir y
probar formalmente).
■Propósito: Probar una propiedad fundamental sobre la lógica interna del
módulo: que su estado de espera de datos refleja correctamente las
condiciones de la interfaz (petición enviada, datos aún no recibidos). Si
se prueba, da una alta confianza en la lógica de control de la operación
de lectura.
Estos ejemplos ilustran cómo las propiedades formales, compuestas por assertions,
assumptions, cover properties e invariantes, permiten especificar con precisión el
comportamiento deseado, las restricciones del entorno y los escenarios a cubrir, sirviendo
como la especificación formal rigurosa que la herramienta de FV verifica contra el diseño.

Apéndices
Los apéndices de este ebook complementan el contenido principal al ofrecer referencias
rápidas, explicaciones concisas de terminología clave y punteros hacia recursos externos para
aquellos lectores que deseen ampliar sus conocimientos o explorar la aplicación práctica de las
metodologías y análisis descritos. Constituyen una parte invaluable del libro como material de
referencia.
A.1 Glosario de Términos
Un libro técnico como este, que aborda la verificación de hardware a bajo nivel y la seguridad,
inevitablemente utiliza una terminología especializada y una gran cantidad de acrónimos
comunes en la industria de semiconductores. El propósito de un glosario es proporcionar
definiciones concisas y claras de estos términos en el contexto del libro, facilitando la
comprensión, especialmente para lectores que pueden no estar familiarizados con todo el
vocabulario específico o que necesitan recordar rápidamente el significado de un acrónimo. Un glosario efectivo para este ebook incluiría términos y acrónimos fundamentales que han
sido clave en la discusión de cada capítulo. Aquí se enumeran algunos de los términos
esenciales que se encontrarían en un glosario completo, junto con una breve descripción
conceptual de lo que significan en este contexto. Un glosario final y completo debería definirse
a partir de todos los términos técnicos utilizados a lo largo del texto del ebook.
●ASIC: (Application-Specific Integrated Circuit) Circuito integrado diseñado a medida
para una aplicación particular, en contraste con un procesador de propósito general.
Requieren verificación y test exhaustivos debido a sus altos costos de desarrollo y
fabricación de máscaras. ●FPGA: (Field-Programmable Gate Array) Un circuito integrado diseñado para ser
configurado por el cliente o diseñador después de la fabricación. Utilizan bloques
lógicos programables y interconexiones reconfigurables. Aunque programables, su
diseño lógico y su mapeo físico también requieren verificación y análisis a bajo nivel
(timing, física).
●RTL: (Register-Transfer Level) Nivel de abstracción en el diseño de hardware digital que
describe el flujo de datos entre registros (elementos de memoria) y las operaciones
lógicas (transferencias) que se realizan sobre esos datos entre registros. Es la
descripción de diseño de entrada común para la síntesis lógica y la verificación
pre-silicio de alto nivel.
●Netlist: Una descripción de la conectividad de un circuito. Puede ser una Netlist Lógica
(a nivel de compuertas, resultado de la síntesis, mostrando instancias de celdas de
biblioteca y cómo se interconectan) o una Netlist Física (extraída del layout, mostrando
cómo las formas físicas en el silicio están conectadas eléctricamente). Las Netlists son
entradas clave para STA, LVS y análisis físicos.

●Compuerta (Gate): Elemento lógico básico (AND, OR, NOT, flip-flop, etc.)
implementado como una celda estándar a nivel físico. Las netlists a nivel de compuertas
describen el diseño en términos de estas celdas y sus interconexiones.
●Verificación Formal (FV): Metodología basada en técnicas matemáticas y lógicas para
probar o refutar formalmente que un diseño (o modelo) cumple ciertas propiedades
especificadas, explorando sistemáticamente (en algunos casos) todo el espacio de
estados. ●Propiedad (Property): Una especificación formal de comportamiento deseado o
indeseado de un diseño, escrita en lenguajes como SVA o PSL, que se verifica
utilizando herramientas de Verificación Formal o simulación con aserciones.
●Aserción (Assertion): En verificación (formal o simulación), una declaración sobre una
propiedad que se espera que sea verdadera en todo momento (o en momentos
específicos) durante la operación del diseño. Las herramientas verifican si las
aserciones se cumplen. ●SVA: (SystemVerilog Assertions) Un lenguaje de especificación de propiedades basado
en SystemVerilog, ampliamente utilizado para escribir aserciones y propiedades para
verificación formal y basada en simulación.
●PSL: (Property Specification Language) Otro lenguaje estándar para la especificación
de propiedades, utilizable con varios lenguajes de descripción de hardware.
●Model Checking: Una técnica de Verificación Formal que explora sistemáticamente el
espacio de estados de un diseño para determinar si una propiedad es verdadera o si
existe una secuencia de eventos (un "contador-ejemplo" o counterexample) que la viola.
●Equivalence Checking (EC): Técnica de Verificación Formal utilizada para demostrar
matemáticamente que dos descripciones de diseño (por ejemplo, RTL post-síntesis vs.
Netlist de compuertas post-síntesis, o Netlist post-síntesis vs. Netlist post-layout) son
funcionalmente equivalentes, asegurando que las transformaciones no introdujeron
errores lógicos.
●Verificación de Diseño (DV): Amplio término que cubre las metodologías utilizadas
para verificar que un diseño funciona según las especificaciones, a menudo basado en
simulación (dirigida, aleatoria).
●UVM: (Universal Verification Methodology) Una metodología y librería estándar basada
en SystemVerilog para construir entornos de verificación estructurados, reusables y
escalables, ampliamente utilizados en la verificación basada en simulación.
●CRV: (Constrained Random Verification) Técnica de verificación basada en simulación
que utiliza generadores de estímulos aleatorios, pero cuyas salidas están restringidas
por reglas (constraints) definidas por el verificador para dirigir la exploración del espacio
de estados hacia escenarios de prueba interesantes o complejos. ●STA: (Static Timing Analysis) Técnica de análisis que verifica los requisitos de timing
(setup, hold) de un diseño digital analizando los retardos de propagación a lo largo de
todos los caminos lógicos, sin necesidad de simular la funcionalidad. Se realiza a nivel
de netlist de compuertas post-layout con información de parasitarias. ●Setup Time: El tiempo mínimo que una señal de datos debe estar estable en la entrada
D de un flip-flop antes del flanco activo del reloj. STA verifica que este requisito se
cumple en todos los caminos.

●Hold Time: El tiempo mínimo que una señal de datos debe estar estable en la entrada
D de un flip-flop después del flanco activo del reloj. STA verifica que este requisito se
cumple en todos los caminos.
●PVT: (Process, Voltage, Temperature) Las condiciones de operación (variaciones en el
proceso de fabricación del silicio, variaciones en el voltaje de alimentación, variaciones
en la temperatura de operación) que afectan los retardos de propagación de las celdas
y cables. STA se realiza en múltiples esquinas PVT. ●OCV: (On-Chip Variation) Variaciones de proceso, voltaje y temperatura que ocurren
dentro del mismo chip, haciendo que celdas idénticas se comporten de forma
ligeramente diferente dependiendo de su ubicación física o su entorno local. STA
avanzado considera OCV. ●Cross-Talk: Acoplamiento capacitivo o inductivo entre cables vecinos que puede afectar
la integridad de la señal y los retardos de propagación, especialmente en
interconexiones a bajo nivel. STA avanzado y análisis de SI (Signal Integrity) lo
consideran. ●Verificación Física: Conjunto de comprobaciones realizadas sobre el layout físico para
asegurar que cumple con las reglas de fabricación y representa correctamente la lógica,
y para extraer información física (parasitarias).
●DRC: (Design Rule Checking) Proceso de verificación física que comprueba que el
layout cumple con las reglas geométricas y de conexión especificadas por la fundición
para garantizar la manufacturabilidad.
●LVS: (Layout Versus Schematic) Proceso de verificación física que compara la netlist
extraída del layout físico con la netlist lógica de origen para asegurar que la
conectividad y los componentes del layout son topológicamente equivalentes al diseño
lógico previsto. ●Extracción de Parasitarias: Proceso que analiza la geometría del layout físico para
calcular las resistencias (R), capacitancias (C) e inductancias (L) parásitas asociadas a
las interconexiones de metal, vías y polígonos. Esta información es crucial para análisis
eléctricos post-layout (STA, SI, IR Drop). ●IR Drop: Caída de voltaje en la red de alimentación (VDD/GND) del chip debido a la
resistencia de los cables y el consumo de corriente de las celdas. El IR Drop excesivo
puede ralentizar las celdas y causar fallos de timing. Se verifica mediante análisis de
potencia estáticos y dinámicos. ●Confiabilidad (Reliability): La capacidad de un chip para funcionar correctamente
durante su vida útil esperada en las condiciones operativas especificadas. Los análisis
de confiabilidad a nivel físico verifican mecanismos de degradación.
●Electromigración (EM): Mecanismo de degradación en interconexiones metálicas
donde el flujo de electrones a alta densidad de corriente y temperatura puede causar el
transporte de átomos de metal, formando huecos y potencialmente interrupciones en los
cables. ●Degradación de Transistores (HCI, NBTI): Mecanismos de degradación que afectan la
performance y fiabilidad de los transistores con el tiempo debido al estrés eléctrico y
térmico, alterando sus características.

●DFT: (Design For Test) Técnicas de diseño que se implementan en el chip para facilitar
las pruebas de fabricación y mejorar su eficiencia y cobertura. Scan Chains es una
técnica DFT clave.
●Scan Chain: Una cadena serial de flip-flops escaneables implementada para permitir
cargar y descargar serialmente el estado interno del diseño en modo de prueba,
facilitando la detección de fallos internos.
●ATPG: (Automatic Test Pattern Generation) Software que genera automáticamente los
patrones de prueba (secuencias de entrada, relojes, valores esperados de salida) para
detectar fallos de fabricación específicos (basados en modelos de fallo) utilizando
estructuras DFT como scan chains. ●Modelo de Fallo (Fault Model): Una representación simplificada de un tipo de defecto
físico en el silicio (ej. stuck-at, transition, bridge) utilizada por las herramientas de test
(como ATPG) para generar patrones de prueba dirigidos a detectar esos defectos.
●Stuck-at Fault: Modelo de fallo donde un nodo (cable o pin) está permanentemente
atascado a un valor lógico fijo (0 o 1).
●Delay Fault: Fallo de retardo. Defecto que causa que la propagación de la señal a lo
largo de un camino sea más lenta de lo esperado, pudiendo causar fallos de timing a
velocidad operativa.
●Timing Aware Scan (At-Speed Test): Prueba de scan que ejecuta la fase de captura a
la velocidad de operación objetivo del chip para detectar fallos de retardo.
●IDDQ Test: Prueba paramétrica que mide la corriente de alimentación quiescente
(estática) del chip en diferentes estados lógicos para detectar fugas excesivas causadas
por ciertos defectos de fabricación (como puentes resistivos).
●Yield: (Rendimiento) El porcentaje de chips funcionales obtenidos de una oblea o lote
de producción. El análisis de rendimiento basado en datos de test ayuda a identificar y
mitigar las causas de los fallos.
●DPM: (Defects Per Million) Número de chips defectuosos por cada millón de unidades
producidas o enviadas. Un objetivo clave de las pruebas de fabricación es lograr un bajo
DPM.
●Hardware Trojan: Una modificación maliciosa (lógica adicional, alteración) introducida
en el diseño o la cadena de suministro del hardware con fines nefastos (por ejemplo,
exfiltrar información, negar servicio, permitir acceso no autorizado).
●Side-Channel Attack (SCA): Ataque que explota información "lateral" (emanaciones
físicas como consumo de potencia, timing, emisiones EM) de un dispositivo para inferir
información secreta (como claves criptográficas) sin atacar directamente los algoritmos
o la lógica. ●Fault Injection: Técnicas (físicas o simuladas) para introducir deliberadamente fallos
(transitorios o permanentes) en un dispositivo para probar su robustez o para intentar
explotar vulnerabilidades de seguridad.
●Sign-off: El proceso formal de aprobación de un diseño en cada etapa mayor (ej.
sign-off de RTL, sign-off de Timing, sign-off de Verificación Física) para proceder a la
siguiente etapa del flujo (ej. fabricación). Pasar LVS y STA limpio es típicamente parte
del sign-off físico.

Un glosario completo proporcionaría definiciones claras y concisas para estos y otros términos
técnicos que se encuentren en el libro.
Acerca de la Autora
Carmen Estela Silva H. es ingeniera e investigadora con más de una década de experiencia
en el ámbito del diseño y verificación de hardware, especializada en ASICs, FPGAs y sistemas
embebidos críticos. Su trayectoria combina la precisión técnica con un profundo compromiso
ético en el desarrollo de tecnologías seguras, confiables y sostenibles.
Ha liderado proyectos de verificación formal y de seguridad en empresas tecnológicas de alto
impacto, integrando metodologías avanzadas para garantizar la corrección funcional y la
integridad del hardware a nivel de silicio. Además, ha contribuido a la divulgación del
conocimiento técnico mediante publicaciones, talleres y materiales educativos orientados a
formar una nueva generación de profesionales capaces de dominar la complejidad del
hardware moderno. A través de TechEbooks, Carmen Estela busca compartir su experiencia de forma práctica y
accesible, acercando la verificación de hardware a ingenieros, investigadores y estudiantes que
aspiran a dominar los fundamentos que sostienen la confiabilidad tecnológica en la era de la
inteligencia artificial y la automatización.
Conclusión Parcial
La verificación de hardware no es solo una etapa técnica dentro del flujo de diseño: es el eje
que define la confiabilidad, seguridad y viabilidad de todo sistema electrónico. Este recorrido
inicial —desde los desafíos de complejidad hasta los fundamentos del bajo nivel— permite
comprender la magnitud del reto y la importancia de aplicar metodologías rigurosas.
La versión completa de este ebook profundiza en las metodologías avanzadas, las técnicas de
verificación formal, los flujos de simulación y los mecanismos de aseguramiento de seguridad a
nivel físico y funcional.

?????? Explora la guía completa en:
https://www.techebooks.online/2025/05/verificacion-de-hardware-asicfpga.html

© 2025 TechEbooks · www.techebooks.online

Verificación de Hardware ASIC FPGA De la Complejidad al Dominio — Versión Parcial de Cortesía.pdf

About This Presentation

Slide Content

Tags

Categories

Download

Quick Actions

Statistics

Related Slideshows

Verificación de Hardware ASIC FPGA De la Complejidad al Dominio — Versión Parcial de Cortesía.pdf

About This Presentation

Slide Content

Slide 2

Slide 3

Slide 4

Slide 5

Slide 6

Slide 7

Slide 8

Slide 9

Slide 10

Slide 11

Slide 12

Slide 13

Slide 14

Slide 15

Slide 16

Slide 17

Slide 18

Slide 19

Slide 20

Slide 21

Slide 22

Slide 23

Slide 24

Slide 25

Slide 26

Slide 27

Slide 28

Slide 29

Slide 30

Slide 31

Slide 32

Slide 33

Slide 34

Slide 35

Slide 36

Slide 37

Slide 38

Slide 39

Slide 40

Slide 41

Slide 42

Slide 43

Slide 44

Slide 45

Slide 46

Slide 47

Slide 48

Slide 49

Slide 50

Slide 51

Slide 52

Slide 53

Slide 54

Slide 55

Slide 56

Slide 57

Slide 58

Slide 59

Slide 60

Slide 61

Slide 62

Slide 63

Tags

Categories

Download

Quick Actions

Statistics

Related Slideshows

8-top-ai-courses-for-customer-support-representatives-in-2025.pptx

7-essential-ai-courses-for-call-center-supervisors-in-2025.pptx

25-essential-ai-courses-for-user-support-specialists-in-2025.pptx

8-essential-ai-courses-for-insurance-customer-service-representatives-in-2025.pptx

Know for Certain

PPT OPD LES 3ertt4t4tqqqe23e3e3rq2qq232.pptx