Skip to Main content Skip to Navigation
Conference papers

Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories

Abstract : For a system-on-chip design which may be composed of multiple processing elements running in parallel, improper execution order and communication assignment may lead to problematic consequences, and one of the consequences could be deadlock. In this paper, we propose an approach to abstracting SpecC-based system models for formal analysis using satisfiability modulo theories (SMT). Based on the language execution semantics, our approach abstracts the timing relations between the time intervals of the behaviors in the design. We then use a SMT solver to check if there are any conflicts among those timing relations. If a conflict is detected, our tool will read the unsatisfiable model generated by the SMT solver and report the cause of the conflict to the user. We demonstrate our approach on a JPEG encoder design model.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, February 13, 2017 - 4:38:23 PM
Last modification on : Thursday, March 5, 2020 - 5:40:30 PM
Long-term archiving on: : Sunday, May 14, 2017 - 3:12:12 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Che-Wei Chang, Rainer Dömer. Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories. 4th International Embedded Systems Symposium (IESS), Jun 2013, Paderborn, Germany. pp.116-127, ⟨10.1007/978-3-642-38853-8_11⟩. ⟨hal-01466667⟩



Record views


Files downloads