Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories
Formal Deadlock Analysis of SpecC Models Using Satisfiability Modulo Theories
复制标题
使用可满足性模理论对 SpecC 模型进行形式化死锁分析
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
R. Dömer
中科院分区：
文献类型：
--
作者：
Che;R. Dömer
对于可能由多个并行运行的处理元件组成的片上系统设计来说，不恰当的执行顺序和通信分配可能会导致问题，其中一个后果就是死锁。在本文中，我们提出了一种方法，利用可满足性模态理论（SMT）对基于 SpecC 的系统模型进行抽象，以便进行形式分析。基于语言执行语义，我们的方法抽象出了设计中行为时间间隔之间的时序关系。然后，我们使用 SMT 求解器检查这些时序关系之间是否存在冲突。如果检测到冲突，我们的工具将读取 SMT 求解器生成的不可满足模型，并向用户报告冲突的原因。我们在 JPEG 编码器设计模型上演示了我们的方法。
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.