Publications
Publications avec comités de relecture
DATICS-IMECS'11
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.
DATICS-IMECS'10
A Formal Model Of SystemC Components Using Fractal Hypergraphs
Award: Certificate of Merit
Abstract:
Abstract:
In this paper, we introduce a new mathematical structure: fractal hypergraph. Due to the hierarchical
and compositional nature of fractal hypergraphs, representations based on fractal hypergraphs
can capture and abstract the object-oriented nature of SystemC. We propose a formal semantics of SystemC
components based on fractal hypergraphs that has already be used in a formal debugger of SystemC components.
DATICS-ICC'08
On the design of a Formal Debugger for System Architecture
Abstract:
System level design helps alleviate much of the burden of usual RTL level design except verification.
Functional verification of system architecture may first seem easier at the higher level of abstraction. In fact,
insight on fundamental aspects of semantics of system level design and impact on lower levels of abstraction
makes it much harder. Formal verification has received till now little attention for functional verification of system
architecture. However, formal verification may provide great benefits to the system level designers. In this paper,
starting from the experiments we have conducted with analyzing and verifying SystemC models using formal
verification techniques, we describe what a potentially very useful approach to build a formal debugger to verify
system architectures designed using a modern system model language like SystemC or SystemVerilog.
Publications invitées
CISST'09
How an "Incoherent Behavior" inside generic hardware component characterizes functional errors ?
Abstract:
Detecting functional errors on generic hardware components is often a complex task. This task becomes
more complex in a componentwise approach when analyzing components without their embedded context that
is the entire system description. In this paper, we propose a methodology that successfully detects just from the
component's description a pure functional error that neither extensive tests nor formal methods could find.