ACCESS: HW/SW-Co-Equivalence Checking for Firmware Optimization

Conference: MBMV 2019 - 22. Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen“
04/08/2019 - 04/08/2019 at Kaiserslautern, Deutschland

Proceedings: MBMV 2019

Pages: 4Language: englishTyp: PDF

Personal VDE Members are entitled to a 10% discount on this title

Schwarz, Michael; Stoffel, Dominik; Kunz, Wolfgang (TU Kaiserslautern, Germany)

Customizing embedded computing platforms to specific application domains often necessitates optimizing the firmware and/or the HW/SW interface under tight resource constraints. Such optimizations frequently alter the communication between the firmware and the peripheral devices, possibly compromising functional correctness of the input/output behavior of the embedded system. This paper proposes a formal HW/SW co-equivalence checking technique for verifying correct I/O behavior of peripherals under a modified firmware.