[ca] L'objectiu d'aquest projecte és construir un sistema de correcció automàtica de circuits digitals i desplegar-lo a Jutge.org, permetent a qualsevol persona aprendre sobre circuits digitals dissenyant-los, provant-los i validant-los sense que una persona faci l'avaluació manual. En conseqüència, el sistema resultant té el potencial de ser utilitzat en cursos de disseny de circuits, proporcionant una plataforma on els professors poden crear els seus propis problemes, i els estudiants poden resoldre'ls i rebre retroalimentació de manera automatitzada. Durant l'avaluació, la solució dels estudiants es compara directament amb la solució de referència sense haver de recórrer als tradicionals casos de prova. Així doncs, el sistema fa una correcció més exhaustiva verificant la correcció per a totes les entrades possibles i detectant problemes que, altrament, podrien haver passat desapercebuts. Tot i això, el nombre d'estats a comprovar creix exponencialment i, per garantir que la correcció es realitza de forma eficient sense sacrificar la fiabilitat, s'utilitzen tècniques de verificació formal per identificar casos concrets en què falla un disseny. Aquesta estratègia proporciona avaluacions precises alhora que proporciona als estudiants informació clara sobre les situacions en què el disseny difereix del comportament esperat sense revelar-ne la solució. Per facilitar que qualsevol persona en el disseny de circuits digitals, aquest projecte també proporciona una eina que permet als usuaris de Jutge.org construir els circuits visualment a través d'una interfície d'arrossegar i deixar anar, i enviar-los directament a Jutge.org sense necessitat que els usuaris escriguin codi en cap moment, millorant encara més l'experiència educativa

[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.