@inproceedings{ddfa94b4a8e6448ba9072e2ea0db9bcf,
title = "Extracting logical formulae that capture the functionality of systemC designs",
abstract = "Object-oriented hardware design languages like SystemC have become very popular to co-design hardware and software systems. Such designs are classically translated into a transition system in order to verify a specification with model-checkers. However, compositionnality and parametricity of SystemC components complicate their translations into finite transition systems. Processing analysis of high-level designs occurs early in the design flow and aims to greatly reduce the correction costs of eventual errors. In this paper, we propose a formal method to statically analyze SystemC designs. Our approach consists in extracting a logical formula representing the behavior of the system in order to avoid combinatorial explosion. This method combines a symbolic execution of SystemC code to infer logical formulae representing its behavior and a generalization phase of these inferred logical properties.",
keywords = "Abstract interpretation, Hypergraphs, Symbolic execution, SystemC",
author = "Nicolas Vall{\'e}e and Bruno Monsuez and Paun, \{Vladimir Alexandru\}",
year = "2011",
month = jul,
day = "26",
language = "English",
isbn = "9789881925121",
series = "IMECS 2011 - International MultiConference of Engineers and Computer Scientists 2011",
pages = "1055--1061",
booktitle = "IMECS 2011 - International MultiConference of Engineers and Computer Scientists 2011",
note = "International MultiConference of Engineers and Computer Scientists 2011, IMECS 2011 ; Conference date: 16-03-2011 Through 18-03-2011",
}