Open Technologies in Formal Verification: Transforming Code for Circuit Validation
Resumo
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.
Palavras-chave:
bounded model checking, VHDL, hardware
Referências
U. B. K. Ramesh, S. Sentilles, and I. Crnkovic, “Energy management in embedded systems: Towards a taxonomy,” in Proceedings of the First International Workshop on Green and Sustainable Software. IEEE Press, 2012.
G. Cabodi, C. Loiacono, M. Palena, P. Pasini, D. Patti, S. Quer, D. Vendraminetto, A. Biere, and K. Heljanko, “Hardware model checking competition 2014: an analysis and comparison of solvers and benchmarks,” Journal on Satisfiability, Boolean Modeling and Computation, 2016.
G1. (2012) Acidente foi provocado por falha em circuito eletrônico, diz secretário. [Online]. Available: [link]
H. Rocha, H. Ismail, L. Cordeiro, and R. Barreto, “Model checking embedded c software using k-induction and invariants (extended version),” arXiv preprint arXiv:1509.02471, 2015.
H. Rocha, L. Cordeiro, R. Barreto, and J. Netto, “Exploiting safety properties in bounded model checking for test cases generation of c programs,” 4th Brazilian Workshop on Systematic and Automated Software Testing (SAST), 2010.
F. Muttenthaler, S. Wilker, and T. Sauter, “Lean automated hardware/-software integration test strategy for embedded systems,” in 22nd IEEE International Conference on Industrial Technology (ICIT), 2021.
R. S. Menezes, M. Aldughaim, B. Farias, X. Li, E. Manino, F. Shmarov, K. Song, F. Brauße, M. R. Gadelha, N. Tihanyi, K. Korovin, and L. C. Cordeiro, “Esbmc v7.4: Harnessing the power of intervals: (competition contribution),” in Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2024.
M. Boule and Z. Zilic, “Efficient automata-based assertion-checker synthesis of seres for hardware emulation,” in Proceedings of the 2007 Asia and South Pacific Design Automation Conference. IEEE Computer Society, 2007.
D. Cappelatti, Praticando VHDL. Editora Feevale, 2010.
I. Grobelna, “Formal verification of control modules in cyber-physical systems,” Sensors, 2020.
C. Baier, J.-P. Katoen, and K. G. Larsen, Principles of model checking. MIT press, 2008.
A. Biere, “The aiger and-inverter graph (aig) format,” 2016. [Online]. Available: [link]
S. Gupta, A. John, and M. Kalra, “Assertion based verification using yosys: A case study from nuclear domain,” in Proceedings of the 16th Innovations in Software Engineering Conference. Association for Computing Machinery, 2023.
L. Cordeiro, B. Fischer, and J. Marques-Silva, “Smt-based bounded model checking for embedded ansi-c software,” IEEE Transactions on Software Engineering, 2012.
D. Thomas and P. Moorby, The Verilog Hardware Description Language. Springer US, 2008.
IEEE, “Iec/ieee international standard - behavioural languages - part 1-1: Vhdl language reference manual,” IEC 61691-1-1:2011(E) IEEE Std 1076-2008, 2011.
——, “Ieee standard for verilog hardware description language,” IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001), 2006.
——, “Ieee standard for standard systemc language reference manual,” IEEE Std 1666-2011 (Revision of IEEE Std 1666-2005), 2012.
E. Christen and K. Bakalar, “Vhdl-ams-a hardware description language for analog and mixed-signal applications,” IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing, 1999.
K. Asanović, R. Avizienis, J. Bachrach, S. Beamer, D. Biancolin, C. Celio, H. Cook, D. Dabbelt, J. Hauser, A. Izraelevitz, S. Karandikar, B. Keller, D. Kim, J. Koenig, Y. Lee, E. Love, M. Maas, A. Magyar, H. Mao, M. Moreto, A. Ou, D. A. Patterson, B. Richards, C. Schmidt, S. Twigg, H. Vo, and A. Waterman, “The rocket chip generator,” Tech. Rep., Apr 2016. [Online]. Available: [link]
R. Mukherjee, M. Tautschnig, and D. Kroening, “v2c – a verilog to c translator,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2016.
D. Beyer and M. E. Keremoglu, “Cpachecker: A tool for configurable software verification,” in International Conference on Computer Aided Verification. Springer, 2011.
R. Mukherjee, P. Schrammel, D. Kroening, and T. Melham, “Unbounded safety verification for hardware using software analyzers,” in Conference on Design, Automation & Test in Europe. EDA Consortium, 2016.
A. F. Donaldson, L. Haller, D. Kroening, and P. Rümmer, “Software verification using k-induction,” in International Static Analysis Symposium. Springer, 2011.
A. Bara, P. Bazargan-Sabet, R. Chevallier, D. Ledu, E. Encrenaz, and P. Renault, “Formal verification of timed vhdl programs,” in Forum on Specification & Design Languages (FDL). IET, 2010.
A. David, P. G. Jensen, K. G. Larsen, M. Mikuˇcionis, and J. H. Taankvist, “Uppaal stratego,” in Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2015.
G. Di Guglielmo, L. Di Guglielmo, F. Fummi, and G. Pravadelli, “On the use of assertions for embedded-software dynamic verification,” in Design and Diagnostics of Electronic Circuits & Systems (DDECS). IEEE, 2012.
A. Gatti and C. Ghezzi, “Vhdl 2 c: Studio e realizzazione di una tecnica di traduzione automatica del vhdl in linguagio c,” [link], Julho 1995.
G. Cabodi, C. Loiacono, M. Palena, P. Pasini, D. Patti, S. Quer, D. Vendraminetto, A. Biere, and K. Heljanko, “Hardware model checking competition 2014: an analysis and comparison of solvers and benchmarks,” Journal on Satisfiability, Boolean Modeling and Computation, 2016.
G1. (2012) Acidente foi provocado por falha em circuito eletrônico, diz secretário. [Online]. Available: [link]
H. Rocha, H. Ismail, L. Cordeiro, and R. Barreto, “Model checking embedded c software using k-induction and invariants (extended version),” arXiv preprint arXiv:1509.02471, 2015.
H. Rocha, L. Cordeiro, R. Barreto, and J. Netto, “Exploiting safety properties in bounded model checking for test cases generation of c programs,” 4th Brazilian Workshop on Systematic and Automated Software Testing (SAST), 2010.
F. Muttenthaler, S. Wilker, and T. Sauter, “Lean automated hardware/-software integration test strategy for embedded systems,” in 22nd IEEE International Conference on Industrial Technology (ICIT), 2021.
R. S. Menezes, M. Aldughaim, B. Farias, X. Li, E. Manino, F. Shmarov, K. Song, F. Brauße, M. R. Gadelha, N. Tihanyi, K. Korovin, and L. C. Cordeiro, “Esbmc v7.4: Harnessing the power of intervals: (competition contribution),” in Tools and Algorithms for the Construction and Analysis of Systems. Springer-Verlag, 2024.
M. Boule and Z. Zilic, “Efficient automata-based assertion-checker synthesis of seres for hardware emulation,” in Proceedings of the 2007 Asia and South Pacific Design Automation Conference. IEEE Computer Society, 2007.
D. Cappelatti, Praticando VHDL. Editora Feevale, 2010.
I. Grobelna, “Formal verification of control modules in cyber-physical systems,” Sensors, 2020.
C. Baier, J.-P. Katoen, and K. G. Larsen, Principles of model checking. MIT press, 2008.
A. Biere, “The aiger and-inverter graph (aig) format,” 2016. [Online]. Available: [link]
S. Gupta, A. John, and M. Kalra, “Assertion based verification using yosys: A case study from nuclear domain,” in Proceedings of the 16th Innovations in Software Engineering Conference. Association for Computing Machinery, 2023.
L. Cordeiro, B. Fischer, and J. Marques-Silva, “Smt-based bounded model checking for embedded ansi-c software,” IEEE Transactions on Software Engineering, 2012.
D. Thomas and P. Moorby, The Verilog Hardware Description Language. Springer US, 2008.
IEEE, “Iec/ieee international standard - behavioural languages - part 1-1: Vhdl language reference manual,” IEC 61691-1-1:2011(E) IEEE Std 1076-2008, 2011.
——, “Ieee standard for verilog hardware description language,” IEEE Std 1364-2005 (Revision of IEEE Std 1364-2001), 2006.
——, “Ieee standard for standard systemc language reference manual,” IEEE Std 1666-2011 (Revision of IEEE Std 1666-2005), 2012.
E. Christen and K. Bakalar, “Vhdl-ams-a hardware description language for analog and mixed-signal applications,” IEEE Transactions on Circuits and Systems II: Analog and Digital Signal Processing, 1999.
K. Asanović, R. Avizienis, J. Bachrach, S. Beamer, D. Biancolin, C. Celio, H. Cook, D. Dabbelt, J. Hauser, A. Izraelevitz, S. Karandikar, B. Keller, D. Kim, J. Koenig, Y. Lee, E. Love, M. Maas, A. Magyar, H. Mao, M. Moreto, A. Ou, D. A. Patterson, B. Richards, C. Schmidt, S. Twigg, H. Vo, and A. Waterman, “The rocket chip generator,” Tech. Rep., Apr 2016. [Online]. Available: [link]
R. Mukherjee, M. Tautschnig, and D. Kroening, “v2c – a verilog to c translator,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2016.
D. Beyer and M. E. Keremoglu, “Cpachecker: A tool for configurable software verification,” in International Conference on Computer Aided Verification. Springer, 2011.
R. Mukherjee, P. Schrammel, D. Kroening, and T. Melham, “Unbounded safety verification for hardware using software analyzers,” in Conference on Design, Automation & Test in Europe. EDA Consortium, 2016.
A. F. Donaldson, L. Haller, D. Kroening, and P. Rümmer, “Software verification using k-induction,” in International Static Analysis Symposium. Springer, 2011.
A. Bara, P. Bazargan-Sabet, R. Chevallier, D. Ledu, E. Encrenaz, and P. Renault, “Formal verification of timed vhdl programs,” in Forum on Specification & Design Languages (FDL). IET, 2010.
A. David, P. G. Jensen, K. G. Larsen, M. Mikuˇcionis, and J. H. Taankvist, “Uppaal stratego,” in Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 2015.
G. Di Guglielmo, L. Di Guglielmo, F. Fummi, and G. Pravadelli, “On the use of assertions for embedded-software dynamic verification,” in Design and Diagnostics of Electronic Circuits & Systems (DDECS). IEEE, 2012.
A. Gatti and C. Ghezzi, “Vhdl 2 c: Studio e realizzazione di una tecnica di traduzione automatica del vhdl in linguagio c,” [link], Julho 1995.
Publicado
22/10/2025
Como Citar
OLIVEIRA, Kevin; ROCHA, Herbert; URQUIZA, Marcelle; NOBRE, Francisco.
Open Technologies in Formal Verification: Transforming Code for Circuit Validation. In: CONGRESSO LATINO-AMERICANO DE SOFTWARE LIVRE E TECNOLOGIAS ABERTAS (LATINOWARE), 22. , 2025, Foz do Iguaçu/PR.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2025
.
p. 253-262.
DOI: https://doi.org/10.5753/latinoware.2025.16325.
