[en] The goal of this project is to build an automatic correction system for digital circuits and deploy it to Jutge.org, allowing anyone to learn about digital circuits by designing, testing, and validating them without needing a person to do the manual evaluation. Thus, the resulting system has the potential to be used in circuit design courses, providing a platform where professors can create their own problems, and students can solve them and receive automated feedback. During the evaluation, the student's solution is compared directly to the reference solution without having to rely on the traditional test cases. Hence, the system performs a more exhaustive correction by verifying the correctness for all possible inputs and detecting issues that could have otherwise remained undetected. However, the number of states to check grows exponentially, and to guarantee that the correction is done efficiently without sacrificing reliability, formal verification techniques are employed to identify specific cases in which a design fails. This approach provides accurate assessments while giving students clear feedback about the situations in which the design differs from the expected behavior without revealing the solution. To facilitate anyone's journey in digital circuit design, this project also provides a tool that allows users of Jutge.org to build the circuits visually through a drag-and-drop interface in a user friendly application and submit them directly to Jutge.org without requiring users to write code at any point, enhancing the educational experience further.

[es] El objetivo de este proyecto es construir un sistema de corrección automática de circuitos digitales y desplegarlo en Jutge.org, permitiendo a cualquiera persona aprender sobre circuitos digitales diseñándolos, probándolos y validándolos sin necesidad de que una persona realice la evaluación manual. Por ende, el sistema resultante tiene el potencial de ser utilizado en cursos de diseño de circuitos, proporcionando una plataforma donde los profesores pueden crear sus propios problemas, y los estudiantes pueden resolverlos y recibir feedback de forma automatizada. Durante la evaluación, la solución del estudiante se compara directamente con la solución de referencia sin tener que recurrir a los casos de prueba tradicionales. De este modo, el sistema realiza una corrección más exhaustiva verificando la corrección para todas las entradas posibles y detectando problemas que, de otro modo, podrían haber pasado desapercibidos. Sin embargo, el número de estados a comprobar crece exponencialmente y, para garantizar que la corrección se realiza de forma eficiente sin sacrificar la fiabilidad, se emplean técnicas de verificación formal para identificar casos concretos en los que falla un diseño. Esta estrategia proporciona evaluaciones precisas a la vez que proporciona a los estudiantes información clara sobre las situaciones en las que el diseño difiere del comportamiento esperado sin revelar la solución. Para facilitar que cualquier persona en el diseño de circuitos digitales, este proyecto también proporciona una herramienta que permite a los usuarios de Jutge.org construir los circuitos visualmente a través de una interfaz de arrastrar y soltar, y enviarlos directamente a Jutge.org sin necesidad de que los usuarios escriban código en ningún momento, mejorando aún más la experiencia educativa.