Compositional Reasoning for Hardware/Software Co-verification

In this paper, we present and illustrate an approach to compositional reasoning for hardware/software co-verification of embedded systems. The major challenges in compositional reasoning for co-verification include: (1) the hardware/software semantic gaps, (2) lack of common property specification languages for hardware and software, and (3) lack of compositional reasoning rules that are applicable across the hardware/software boundaries. Our approach addresses these challenges by (1) filling the hardware/software semantic gaps via translation of hardware and software into a common formal language, (2) defining a unified property specification language for hardware, software, and entire systems, and (3) enabling application of existing compositional reasoning rules across the hardware/software boundaries based on translation, developing a new rule for compositional reasoning with components that share sub-components, and extending the applicability of these rules via dependency refinem...

• Type: Conference
• Year: 2006
• Where: ATVA
• Authors: Fei Xie, Guowu Yang, Xiaoyu Song
• Keywords: ATVA 2006, Compositional Reasoning, Compositional Reasoning Rules, Hardware, Hardware/software Semantic Gaps