Open Technologies in Formal Verification: Transforming Code for Circuit Validation - Oliveira, Kevin; Rocha, Herbert; Urquiza, Marcelle; Nobre, Francisco (Anais do Congresso Latino-Americano de Software Livre e Tecnologias Abertas (Latinoware); 2025: Anais do XXII Congresso Latino-Americano de Software Livre e Tecnologias AbertasDO - 10.5753/latinoware.2025.16325, 2025)
This study introduces a methodology for the formal verification of logic circuits described in VHDL, leveraging code transformation and assertion-based property validation. The proposed workflow automatically translates VHDL code into C, enabling the use of advanced analysis tools such as ESBMC, which applies bounded model checking and k-induction techniques. Two translation strategies are presented: a direct approach utilizing a single tool, and a multiple-tool approach that combines distinct translators to improve compatibility with complex VHDL constructs. Code instrumentation ensures that assertions are accurately mapped and verified within the C environment. Experimental evaluation using established benchmarks demonstrates that the multiple-tool approach provides greater flexibility and a higher success rate in both translation and circuit analysis. The results confirm the effectiveness of the methodology in detecting errors and validating safety properties in hardware designs, thereby enhancing the reliability of embedded systems.