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 metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01466667
Contributor : Hal Ifip <>
Submitted on : Monday, February 13, 2017 - 4:38:23 PM
Last modification on : Wednesday, August 7, 2019 - 12:14:02 PM
Long-term archiving on : Sunday, May 14, 2017 - 3:12:12 PM

File

978-3-642-38853-8_11_Chapter.p...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

82

Files downloads

237