Botella Juan, GuillermoMagalló Paz, Álvaro2025-09-182025-09-182025https://hdl.handle.net/20.500.14352/124125Trabajo de Fin de Grado en Ingeniería Informática, Facultad Informática UCM, Dpto. de Arquitectura de Computadores y Automática, Curso 2024/2025Este trabajo presenta el diseño y verificación de un sistema neuromórfico mixto basado en el modelo de Izhikevich, empleando ́técnicas de verificación ́ formal y simulación electrónica. Se desarrolla un entorno simbólico en Python que permite representar circuitos hardware mediante restricciones lógicas, las cuales son verificadas automáticamente mediante el resolutor SMT Z3. Asimismo, se implementa un banco de pruebas hardware en Siemens PartQuest, que recorre de forma determinista el espacio de entradas para garantizar el cumplimiento funcional. La propuesta sigue los principios establecidos por los estándares DO-254 y DO-333, integrando la trazabilidad normativa, la validación funcional y la comprobación lógica en un mismo entorno. El trabajo demuestra la viabilidad de una metodología combinada basada en modelado simbólico, verificación automatizada y simulación exhaustiva de hardware.This work presents the design and verification of a mixed neuromorphic system based on the Izhikevich model, using formal verification techniques and electronic simulation. A symbolic environment in Python is developed, allowing hardware circuits to be represented through logical constraints, which are automatically verified using the Z3 SMT solver. Additionally, a hardware testbench is implemented in Siemens PartQuest, deterministically exploring the input space to ensure functional compliance. The proposed approach follows the principles of the DO-254 and DO-333 standards, integrating regulatory traceability, functional validation, and logical verification within a unified environment. The project demonstrates the feasibility of a combined methodology based on symbolic modeling, automated verification, and exhaustive hardware simulation.spaAttribution-NonCommercial-NoDerivatives 4.0 Internationalhttp://creativecommons.org/licenses/by-nc-nd/4.0/bachelor thesisopen access004(043.3)Hardware neuromórficoVerificacion formalZ3VHDL-AMSSimulación electrónicaSistemas críticosDO-254Modelado simbolicoLógica temporalArquitectura en pipelineNeuromorphic hardwareFormal verificationZ3VHDL-AMSElectronic simulationSafety-critical systemsDO-254Symbolic modelingTemporal logicPipeline architectureInformática (Informática)33 Ciencias Tecnológicas