 |
System Level Design from HW/SW to Memory for Embedded Systems 5th IFIP TC 10 International Embedded Systems Symposium, IESS 2015 Foz do Iguaçu, Brazil, November 3-6, 2015 |
 |
Conference papers
Bit-Precise Formal Verification for SystemC Using Satisfiability Modulo Theories Solving
Abstract : Hardware/software codesigns are often modeled with the system level design language SystemC. Especially for safety critical applications, it is crucial to guarantee that such a design meets its requirement. In this paper, we present an approach to formally verify SystemC designs using the UCLID satisfiability modulo theories (SMT) solver. UCLID supports finite precision bitvector arithmetics. Thus, we can handle SystemC designs on a bit-precise level, which enables us to formally verify deeply integrated hardware/software systems that comprise detailed hardware models. At the same time, we exploit UCLID’s ability to handle symbolic variables and use k-inductive invariant checking for SystemC designs. With this inductive approach, we can counteract the state space explosion problem, which model checking approaches suffer from. We demonstrate the practical applicability of our approach with a SystemC design that comprises a bit- and cycle-accurate model of a UART and software that reads data from the UART.
Cited literature [16 references]
https://hal.inria.fr/hal-01854165
Contributor : Hal Ifip <>
Submitted on : Monday, August 6, 2018 - 3:10:24 PM
Last modification on : Monday, August 6, 2018 - 3:12:00 PM
Document(s) archivé(s) le : Wednesday, November 7, 2018 - 3:02:16 PM
Contributor : Hal Ifip <>
Submitted on : Monday, August 6, 2018 - 3:10:24 PM
Last modification on : Monday, August 6, 2018 - 3:12:00 PM
Document(s) archivé(s) le : Wednesday, November 7, 2018 - 3:02:16 PM
File
467217_1_En_5_Chapter.pdf
Files produced by the author(s)
Licence
Distributed under a Creative Commons Attribution 4.0 International License
